Changes between Version 39 and Version 40 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 3:32:12 AM (3 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