Changes between Version 13 and Version 14 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 22, 2012 7:47:31 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

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