I was a bit surprised to find out that the * notation in
Definition f (g : Type -> Type) := forall a b, g (a * b).
was interpreted in nat_scope instead of type_scope. Reading up on the docs, I found:
The scope type_scope has a special status. It is a primitive interpretation scope which is temporarily activated each time a subterm of an expression is expected to be a type.
(a * b) is clearly expected to be a type. What am I missing here?
It is "clearly expected to be a type" after typing has occurred, but the resolution of notations happen before typing (for obvious reasons). If
g had not been a local binder but a global symbol, then it would have worked.
Thanks, I see.
If g had not been a local binder but a global symbol, then it would have worked.
Is that because g can then be separately typed and have appropriate scopes bound to its arguments?
Last updated: Jan 29 2023 at 05:03 UTC