Changes between Version 12 and Version 13 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 4:00:22 PM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v12 v13  
    3333 
    3434data IsEven a :: Nat -> * where 
    35   IsEvenZero ::                    IsEven 0 
    36   IsEven     :: !(TNat (n + 1)) -> IsEven (2 * (n + 1)) 
    37   IsOdd      :: !(TNat n)       -> IsEven ((2 * n) + 1) 
     35  IsEvenZero ::              IsEven 0 
     36  IsEven     :: !(TNat n) -> IsEven (2 * n + 2) 
     37  IsOdd      :: !(TNat n) -> IsEven (2 * n + 1) 
    3838}}}