Changes between Version 1 and Version 2 of TypeNats/SingletonsAndExistentials

Show
Ignore:
Timestamp:
04/17/12 13:02:24 (14 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeNats/SingletonsAndExistentials

    v1 v2  
    11Consider a type for arrays with a statically known size. 
    22{{{ 
    3 newtype StaticArray (n :: Nat) a = SA (Ptr a) 
     3newtype ArrPtr (n :: Nat) a = SA (Ptr a) 
    44}}} 
    55 
    … …  
    77{{{ 
    88data ArrayS :: * -> * where 
    9   ArrS :: Sing n -> StaticArray n a -> ArrayS a 
     9  ArrS :: Sing n -> ArrPtr n a -> ArrayS a 
    1010}}} 
    1111 
    1212{{{ 
    1313data ArrayD :: * -> * where 
    14   ArrD :: SingI n => StaticArray n a -> ArrayD a 
     14  ArrD :: SingI n => ArrPtr n a -> ArrayD a 
    1515}}}