Changes between Version 8 and Version 9 of TypeNats/Basics

Timestamp:

01/16/11 09:54:12 (2 years ago)

Author:

diatchki

Comment:

--

TypeNats/Basics

@@ -21 +21 @@
 }}}
 The only "interesting" value of type ''Nat n'' is the number ''n''.  Technically, there is also an undefined element.
+The value of a singleton type may be named using ''nat'', which is a bit like a "smart" constructor for ''Nat n''.
+Note that because ''nat'' is polymorphic, we may have to use a type signature to specify which singleton we mean.  For example:
+{{{
+> natToInteger (nat :: Nat 3)
+3
+}}}
 
-One may think of the smart constructor ''nat'' as being a method of a special built-in class:
+One may think of the smart constructor ''nat'' as being a method of a special built-in class, ''NatI'':
 {{{
 class NatI n where
@@ -32 +38 @@
 etc.
 }}}
+
+The name ''NatI'' is a mnemonic for the different uses of the class:
+  * It is the ''introduction'' construct for 'Nat' values,
+  * It is an ''implicit'' parameter of kind 'Nat' (link)
+