The page says:
Function types are written (x : A) → B or A → B for non-dependent functions.
Is the ``for non-dependent functions'' meant to refer to both versions? It sounds like it does.
(x : A) → B
also be written as
(x : A) B
The example two paragraphs in has something of that shape --- what are the precise rules?
Powered by PmWiki