Ali Caglayan (Jan 26 2022 at 19:51): Ali Caglayan (Jan 26 2022 at 19:51):What was the reason we have to use {| instead of {? I can't recall. cc @Hugo Herbelin
Jason Gross (Jan 26 2022 at 19:54):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
Gaëtan Gilbert (Jan 26 2022 at 20:08):{ probably gets confused with the sigma type syntax
Gaëtan Gilbert (Jan 26 2022 at 20:09):I think Instance came after Record
Matthieu Sozeau (Jan 27 2022 at 11:11):Yes, the conflict is with the other notations starting with {, so the various sigma types and sum types using it
Ali Caglayan (Jan 27 2022 at 12:56):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.
Gaëtan Gilbert (Jan 27 2022 at 13:02):parser limitations I guess
Paolo Giarrusso (Jan 27 2022 at 15:46):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: Apr 20 2024 at 02:40 UTC