Changes between Version 13 and Version 14 of TypeNats/Basics
 Timestamp:
 Jan 16, 2011 6:02:19 PM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v13 v14 47 47 == Examples == 48 48 49 Here is how we can use th is APIto define a `Show` instance for singleton types:49 Here is how we can use the basic primitives to define a `Show` instance for singleton types: 50 50 {{{ 51 51 instance Show (Nat n) where … … 55 55 A more interesting example is to define a function which maps integers into singleton types: 56 56 {{{ 57 integerToMaybeNat :: TypeNatn => Integer > Maybe (Nat n)57 integerToMaybeNat :: NatI n => Integer > Maybe (Nat n) 58 58 integerToMaybeNat x = check nat 59 59 where check y = if x == natToInteger y then Just y else Nothing … … 68 68 Now, we can use `integerToNat` to provide a `Read` instance for singleton types: 69 69 {{{ 70 instance TypeNatn => Read (Nat n) where70 instance NatI n => Read (Nat n) where 71 71 readsPrec p x = do (x,xs) < readsPrec p x 72 72 case integerToMaybeNat x of