What was the reason we have to use {|
instead of {
? I can't recall. cc @Hugo Herbelin
I'm not sure if it's still the case, but it used to be the case that {
activated bidirectional typechecking of constructors when used with Instance :=
, which also allows using non-qualified names to refer to non-imported fields
{
probably gets confused with the sigma type syntax
I think Instance came after Record
Yes, the conflict is with the other notations starting with {
, so the various sigma types and sum types using it
I still don't understand how it clashes with those notations however { f := x ; g := y}
doesn't look anything like a sigma or sum type.
parser limitations I guess
when you look at { f := x ; g := y}
the parser sees {f
(because it only has 1 token of look ahead), and that could be either a record or a sigma
Last updated: May 31 2023 at 16:01 UTC