Kenji Maillard (Dec 23 2021 at 18:43): 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 ?
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).
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
*)
That looks like a bug then.
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
Paolo Giarrusso (Dec 24 2021 at 00:56):the useful behavior is covered by this syntax:
Definition foo `{n : nat} : nat := n.
@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]
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.
yes I was talking about that, and I was not aware of the warning...
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: Oct 05 2023 at 02:01 UTC