Changes between Version 13 and Version 14 of TypeNats/Basics
- Timestamp:
- 01/16/11 10:02:19 (2 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
