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.
Can
(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?
Page last modified on November 28, 2009, at 01:22 am
Powered by
PmWiki