I eventually started to use equations (beyond doing the tutorial). I usually avoid using additional tools in production stuff if I get along with what I have, but today I had a rather nasty dependently typed fixpoint and really couldn't figure out how to write the return statement of a match, so I thought "time to try equations". And I must say although I like OCaml style matches over Haskell style function definitions, I really liked it and it was very smooth. Also the proofs got much easier with the tools equations offers. It was almost like when I switched from C++ to OCaml 10 years back and wondered how I could have wasted half of my life writing C++ code.
Keep up the good work!
One thing I missing (or can't figure out) in equations is Haskell/Idris-style as-patterns, i.e., the ability to do something like this:
Equations foo (xs : list A) (t : B) : C := ... foo xs@(x::s) t => foo s (bar xs)
That ones a tricky parsing problem, as equations allows any term/notation on the left-hand side...
@Michael Soegtrop You are tempting me to try Equations :)
@Mukesh Tiwari : this was indeed the point of my post (besides giving kudos to the developers)
Last updated: May 28 2023 at 18:29 UTC