How difficult would it be to drop the need for an end in a match block in coq? I'm wondering since ocaml is able to do so.
That would be a very bad idea, I believe.
The lack of a delimiter for match blocks is a major pain point of OCaml
it's not robust to pattern extension and it's very annoying for nested matches
plus a few more issues with precedence
I've already heard major OCaml developers openly complaining about the OCaml syntax which is notoriously broken, even outside of the core dev circle
Do you remember around when ocaml accepted these kinds of match statements? I'm interested in seeing why they did it.
it's very old
since the inception of the language essentially
caml light already had this syntax IIRC
the grandiose time when internet was not even widely available
OK, so it's unlikely that I am going to find a well thought out argument for them
On a side note, what is our preference on using them in coq ml?
Is it good style to not close matches? I see closed and unclosed ones all them time when reading code, so I am wondering what the preference is
I think that we only close them when necessary
otherwise it's very verbose since you also have to add a
Oh, I didn't know that the begin was necessary
you're talking about OCaml, right?
so yes in OCaml there is no
end block for a
match, this needs to be enclosed in a
Thanks for the info, I will continue on not to think about it too much :-)
or parentheses but I personally find this to be unreadable
(full disclaimer: I believe that LISP is a shibboleth language designed to tell apart humans from stack automata)
Unless we also start to make indentation matter, a terminator for match is very handy. I could live with an exception if it is the outermost one, eg
Definition f x := match x with ... . in some sense the
. would also close the match.
Note that if you load ssreflect you get to write
if n is S p then f p else q which is a binary match with no terminator.
Last updated: Jun 09 2023 at 08:01 UTC