Changes between Version 4 and Version 5 of TypeNats/MatchingOnNats


Ignore:
Timestamp:
Sep 23, 2012 4:04:10 AM (19 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/MatchingOnNats

    v4 v5  
    3636We can solve this problem by providing an additional representation of type-level natural numbers, 
    3737one that has explicit structure.  We define another kind, `Nat1`, which represents natural numbers 
    38 is the traditional unary representation (here we are using GHC's `DataKinds` extension): 
     38in the traditional unary representation (here we are using GHC's `DataKinds` extension): 
    3939{{{ 
    4040data Nat1 = Zero | Succ Nat1