Michael Soegtrop (Apr 21 2022 at 17:49): Michael Soegtrop (Apr 21 2022 at 17:49):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!
Alexander Gryzlov (Apr 21 2022 at 18:03):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...
Mukesh Tiwari (May 07 2022 at 15:26):@Michael Soegtrop You are tempting me to try Equations :)
Michael Soegtrop (May 08 2022 at 08:37):@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