3 ms·
Why define Notation for pairs and then not use it? Instead of using match/with/true/false, you can use if/then/else. Verlang looks great. Will have to try it
by colanderman 13y ago
Why define Notation for pairs and then not use it?
Instead of using match/with/true/false, you can use if/then/else.
Verlang looks great. Will have to try it out.
Strange that Verlang generates uncurried functions. I know that's not the default in Erlang, but as you found out, it breaks extraction.
- cmeiklejohn 13y agoNoted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked. Agreed, could use if. I mainly used match with the true/false branches to make it as close to the original Erlang as possible, for readers unfamiliar with the Coq syntax.