Changes between Version 13 and Version 14 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 22, 2012 7:47:31 AM (2 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}}}