Changes between Version 40 and Version 41 of TypeNats/Basics


Ignore:
Timestamp:
Oct 16, 2012 4:28:45 AM (3 years 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