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: Jun 14 2024 at 19:02 UTC