Stream: Coq devs & plugin devs

Topic: Record `{| f := t |}` syntax


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

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 20:08):

{ probably gets confused with the sigma type syntax

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 20:09):

I think Instance came after Record

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

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

view this post on Zulip Gaëtan Gilbert (Jan 27 2022 at 13:02):

parser limitations I guess

view this post on Zulip 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: Feb 02 2023 at 13:03 UTC