spaceloop (Jun 03 2021 at 08:35): spaceloop (Jun 03 2021 at 08:35):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.
My subterm (a * b) is clearly expected to be a type. What am I missing here?
Guillaume Melquiond (Jun 03 2021 at 08:38):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.
spaceloop (Jun 03 2021 at 08:56):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?
Guillaume Melquiond (Jun 03 2021 at 08:57):Yes, exactly.
Last updated: Oct 01 2023 at 18:01 UTC