The syntax for ∀ is inconsistent with other function types in that it uses . to separate the binding from the body, while ∏ types and non-dependent function types use ->; it’s additionally inconsistent with the rest of the grammar in that it requires non-ASCII characters.
Fixing the former would probably require us to use braces to surround the binding, or else just require parens if you’re trying to do e.g. ∀ x : (Type -> Type) -> ….
Fixing the latter could be done by accepting e.g. \/ or forall, albeit at the expense of introducing a keyword.
The syntax for ∀ is inconsistent with other function types in that it uses
.to separate the binding from the body, while ∏ types and non-dependent function types use->; it’s additionally inconsistent with the rest of the grammar in that it requires non-ASCII characters.Fixing the former would probably require us to use braces to surround the binding, or else just require parens if you’re trying to do e.g.
∀ x : (Type -> Type) -> ….Fixing the latter could be done by accepting e.g.
\/orforall, albeit at the expense of introducing a keyword.