Changes between Version 13 and Version 14 of TypeNats/InductiveDefinitions

Show
Ignore:
Timestamp:
03/22/12 00:47:31 (14 months 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}}}