Changes between Version 5 and Version 6 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 5:33:21 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v5 v6  
    1616{{{ 
    1717data Nat (n :: Nat) 
     18nat          :: NatI n => Nat n 
     19natToInteger :: Nat n -> Integer 
    1820}}} 
    1921The only value of type {{{Nat n}}} is the number {{{n}}}.  (Technically, there is also an undefined element.) 
     
    2325  nat :: Nat n 
    2426 
    25 natToInteger :: Nat n -> Integer 
     27instance NatI 0 where nat = "0" 
     28instance NatI 1 where nat = "1" 
     29instance NatI 2 where nat = "2" 
     30etc. 
    2631}}} 
     32 
     33 
    2734 
    2835== Type-Level Operations ==