Changes between Version 7 and Version 8 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 5:40:04 PM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v7 v8  
    2020natToInteger :: Nat n -> Integer 
    2121}}} 
    22 The only value of type {{{Nat n}}} is the number {{{n}}}.  (Technically, there is also an undefined element.) 
     22The only "interesting" value of type ''Nat n'' is the number ''n''.  Technically, there is also an undefined element. 
    2323 
     24One may think of the smart constructor ''nat'' as being a method of a special built-in class: 
    2425{{{ 
    2526class NatI n where 
    2627  nat :: Nat n 
    2728 
    28 instance NatI 0 where nat = "0" 
    29 instance NatI 1 where nat = "1" 
    30 instance NatI 2 where nat = "2" 
     29instance NatI 0 where nat = "singleton 0 value" 
     30instance NatI 1 where nat = "singleton 1 value" 
     31instance NatI 2 where nat = "singleton 2 value" 
    3132etc. 
    3233}}}