Changes between Version 12 and Version 13 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 4:00:22 PM (3 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}}}