Stream: Coq users

Topic: Curious entry in documentation


view this post on Zulip Kenji Maillard (Dec 23 2021 at 18:43):

The documentation of implicit generalization mentions in its BNF that a name for a binder can be provided inside brackets:

Definition foo `({n} : nat) : nat := n.

By pure curiosity, what's the meaning/purpose of this construction ?

view this post on Zulip Guillaume Melquiond (Dec 23 2021 at 18:52):

It is just the combination of a maximally implicit argument {n} and of a generalizable type `(nat) (except that there is nothing to generalize in nat).

view this post on Zulip Kenji Maillard (Dec 23 2021 at 18:53):

But n doesn't end up as a maximally implicit argument:

Definition foo `({n} : nat) : nat := n.
About foo.
(*
foo : nat -> nat

foo is not universe polymorphic
Arguments foo _%nat_scope
foo is transparent
Expands to: Constant raro.foo
*)

view this post on Zulip Guillaume Melquiond (Dec 23 2021 at 18:55):

That looks like a bug then.

view this post on Zulip Enrico Tassi (Dec 23 2021 at 21:38):

I think coq lets you write {name} deep in a term in binder position, but it simply ignores the curly. Imo this is a shallow instance of that behavior

view this post on Zulip Paolo Giarrusso (Dec 24 2021 at 00:56):

the useful behavior is covered by this syntax:

Definition foo `{n : nat} : nat := n.

view this post on Zulip Paolo Giarrusso (Dec 24 2021 at 00:59):

@Enrico Tassi you mean like in Definition foo : Type := ∀ {U}, U.? That gives a warning at least:

Ignoring implicit binder declaration in unexpected position.
[unexpected-implicit-declaration,syntax]

view this post on Zulip Paolo Giarrusso (Dec 24 2021 at 00:59):

BTW, I'm pleasantly surprised that generalization does compose with non-maximal implicits in the right way!

Definition foo `[n : nat] (x : nat) : nat := n.

view this post on Zulip Enrico Tassi (Dec 24 2021 at 06:56):

yes I was talking about that, and I was not aware of the warning...

view this post on Zulip Kenji Maillard (Dec 24 2021 at 13:34):

Enrico Tassi said:

I think coq lets you write {name} deep in a term in binder position, but it simply ignores the curly. Imo this is a shallow instance of that behavior

When the name is followed by a type, Coq only accept {name : T} and not {name} : T or ({name} : T) which is entirely reasonable but makes the quirk above quite awkward.


Last updated: Feb 06 2023 at 13:03 UTC