Changes between Version 13 and Version 14 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 6:02:19 PM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Basics

    v13 v14  
    4747== Examples == 
    4848 
    49 Here is how we can use this API to define a `Show` instance for singleton types: 
     49Here is how we can use the basic primitives to define a `Show` instance for singleton types: 
    5050{{{ 
    5151instance Show (Nat n) where 
     
    5555A more interesting example is to define a function which maps integers into singleton types: 
    5656{{{ 
    57 integerToMaybeNat :: TypeNat n => Integer -> Maybe (Nat n) 
     57integerToMaybeNat :: NatI n => Integer -> Maybe (Nat n) 
    5858integerToMaybeNat x = check nat 
    5959  where check y = if x == natToInteger y then Just y else Nothing 
     
    6868Now, we can use `integerToNat` to provide a `Read` instance for singleton types: 
    6969{{{ 
    70 instance TypeNat n => Read (Nat n) where 
     70instance NatI n => Read (Nat n) where 
    7171  readsPrec p x       = do (x,xs) <- readsPrec p x 
    7272                           case integerToMaybeNat x of