Changes between Version 13 and Version 14 of TypeNats/Basics


Ignore:
Timestamp:
Jan 16, 2011 6:02:19 PM (5 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