Changes between Version 7 and Version 8 of TypeNats/Basics
 Timestamp:
 Jan 16, 2011 5:40:04 PM (6 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v7 v8 20 20 natToInteger :: Nat n > Integer 21 21 }}} 22 The only value of type {{{Nat n}}} is the number {{{n}}}. (Technically, there is also an undefined element.)22 The only "interesting" value of type ''Nat n'' is the number ''n''. Technically, there is also an undefined element. 23 23 24 One may think of the smart constructor ''nat'' as being a method of a special builtin class: 24 25 {{{ 25 26 class NatI n where 26 27 nat :: Nat n 27 28 28 instance NatI 0 where nat = " 0"29 instance NatI 1 where nat = " 1"30 instance NatI 2 where nat = " 2"29 instance NatI 0 where nat = "singleton 0 value" 30 instance NatI 1 where nat = "singleton 1 value" 31 instance NatI 2 where nat = "singleton 2 value" 31 32 etc. 32 33 }}}