Document areequal and @areequal

[ztangent]

While looking through the docs, I noticed that the areequal and @areequal macros aren't currently documented, and are only briefly mentioned by example in the tutorials and the explanation of equality saturation. It'd be great if docstrings could be added for those methods, since I think they are one of the more useful analyses this package can perform.

(Thanks for this really cool package! I've been using it for some simply term rewriting tasks, and am looking to use it to write an equivalence checker for expressions in a fragment of epistemic modal logic -- hence my question about areequal.)

[0x0f0f0f]

Hi there! Thanks for the very kind words. Are you using v2.0 relese or the ale/3.0 branch? I really recommend the latter for stability and performance improvements.

I am however planning to provide better ergonomics to these two. The macro @areequal is really just a convenience macro for more concise testing, but it makes debugging a copy-paste heavy task, and I was actually thinking of removing it in favor of slighter verbose tests. I will add a docstring for areequal function.

Do you have any ideas to share for better ergonomics/interface?

[ztangent]

I've just been using v2.0 since that's the version available off the General registry! But looking forward to the next release.

I don't have specific ideas re ergonomics -- I mostly needed a fast equivalence checker between symbolic expressions which are generated by some other code (in our case, an LLM translating English to logical formulae, compared against a canonical set of expressions), so that's why areequal seemed like the right function to use.