Changes between Version 14 and Version 15 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Apr 9, 2012 2:14:39 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v14 v15  
    88is useful when using {{{TNat}}} to count something. 
    99{{{ 
    10 isZero :: TNat n -> IsZero n 
     10isZero :: Sing n -> IsZero n 
    1111 
    1212data IsZero :: Nat -> * where 
    1313  IsZero ::              IsZero 0 
    14   IsSucc :: !(TNat n) -> IsZero (n + 1) 
     14  IsSucc :: !(Sing n) -> IsZero (n + 1) 
    1515}}} 
    1616 
     
    3030in half: 
    3131{{{ 
    32 isEven :: TNat n -> IsEven n 
     32isEven :: Sing n -> IsEven n 
    3333 
    3434data IsEven a :: Nat -> * where 
    3535  IsEvenZero ::                  IsEven 0 
    36   IsEven     :: !(TNat (n+1)) -> IsEven (2 * n + 2) 
    37   IsOdd      :: !(TNat n)     -> IsEven (2 * n + 1) 
     36  IsEven     :: !(Sing (n+1)) -> IsEven (2 * n + 2) 
     37  IsOdd      :: !(Sing n)     -> IsEven (2 * n + 1) 
    3838}}}