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}}}