Changes between Version 40 and Version 41 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 4:28:45 AM (18 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v40 v41  
    3434 
    3535But, if we have a value of type `Sing a`, how do we get the actual integer or string? 
    36 We can do this with the function `fromSing`: 
     36We can do this with the overloaded function `fromSing`.  Its type is quite general because 
     37it can support various singleton families, but for the purposes of this explanation 
     38it is sufficient t 
     39 
    3740{{{ 
    38 fromSing :: SingE a => Sing a -> Demote a 
    39  
    40 -- XXX: NOT YET UPDATED 
    41 type family SingRep a 
    42 type instance SingRep (n :: Nat)    = Integer 
    43 type instance SingRep (n :: Symbol) = String 
     41fromSing :: Sing (a :: Nat) -> Integer 
     42fromSing :: Sing (a :: Symbol) -> String 
    4443}}} 
    4544