Changes between Version 39 and Version 40 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 3:32:12 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v39 v40  
    2626of singleton types, parameterized by type-level literals: 
    2727{{{ 
    28 newtype Sing :: a -> * 
     28data Sing :: a -> * 
    2929}}} 
    3030For example, `Sing 0`, `Sing 127`, `Sing "hello"`, and `Sing "this also"` are all 
     
    3636We can do this with the function `fromSing`: 
    3737{{{ 
    38 fromSing :: Sing a -> SingRep a 
     38fromSing :: SingE a => Sing a -> Demote a 
    3939 
     40-- XXX: NOT YET UPDATED 
    4041type family SingRep a 
    4142type instance SingRep (n :: Nat)    = Integer