Stream: Equations devs & users

Topic: New user feedback


view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip Matthieu Sozeau (Apr 25 2022 at 09:40):

That ones a tricky parsing problem, as equations allows any term/notation on the left-hand side...

view this post on Zulip Mukesh Tiwari (May 07 2022 at 15:26):

@Michael Soegtrop You are tempting me to try Equations :)

view this post on Zulip 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: Jan 29 2023 at 16:02 UTC