Changes between Version 4 and Version 5 of TypeNats/Basics


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

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v4 v5  
    1313== Singleton Types == 
    1414 
     15We relate type-level natural numbers to run-time values via a family of singleton types: 
    1516{{{ 
    16 data Nat n 
     17data Nat (n :: Nat) 
     18}}} 
     19The only value of type {{{Nat n}}} is the number {{{n}}}.  (Technically, there is also an undefined element.) 
    1720 
    18 class TypeNat n where 
     21{{{ 
     22class NatI n where 
    1923  nat :: Nat n 
    2024