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?

Page last modified on November 28, 2009, at 01:22 AM
Powered by PmWiki