Changes between Version 8 and Version 9 of TypeNats/Basics
 Timestamp:
 Jan 16, 2011 5:54:12 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v8 v9 21 21 }}} 22 22 The only "interesting" value of type ''Nat n'' is the number ''n''. Technically, there is also an undefined element. 23 The value of a singleton type may be named using ''nat'', which is a bit like a "smart" constructor for ''Nat n''. 24 Note that because ''nat'' is polymorphic, we may have to use a type signature to specify which singleton we mean. For example: 25 {{{ 26 > natToInteger (nat :: Nat 3) 27 3 28 }}} 23 29 24 One may think of the smart constructor ''nat'' as being a method of a special builtin class :30 One may think of the smart constructor ''nat'' as being a method of a special builtin class, ''NatI'': 25 31 {{{ 26 32 class NatI n where … … 32 38 etc. 33 39 }}} 40 41 The name ''NatI'' is a mnemonic for the different uses of the class: 42 * It is the ''introduction'' construct for 'Nat' values, 43 * It is an ''implicit'' parameter of kind 'Nat' (link) 44 34 45 35 46