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?

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?

Yes, exactly.

Last updated: Jun 18 2024 at 21:01 UTC