Changes between Version 4 and Version 5 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 5:29:27 PM (5 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