Changes between Version 8 and Version 9 of TypeNats/InductiveDefinitions


Ignore:
Timestamp:
Mar 21, 2012 1:37:34 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/InductiveDefinitions

    v8 v9  
    3232isEven :: TNat n -> IsEven n 
    3333 
    34 data IsEven $a where 
     34data IsEven a :: Nat -> * where 
    3535  IsEvenZero ::                    IsEven 0 
    3636  IsEven     :: !(TNat (n + 1)) -> IsEven (2 * (n + 1))