Changes between Version 18 and Version 19 of TypeNats/Basics
 Timestamp:
 Jan 31, 2011 9:37:35 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/Basics
v18 v19 59 59 where check y = if x == natToInteger y then Just y else Nothing 60 60 }}} 61 It checks that the value argument `x`, passed at runtime, matches the staticallyexpected value, returning `Nothing` if not, and a typed singleton if so. 61 62 62 63 The implementation of `integerToMaybeNat` is a little subtle: by using … … 64 65 `nat` (aka `y`) both have the same type, namely `Nat n`. There are other 65 66 ways to achieve the same, for example, by using scoped type variables, 66 and providing explicit type signatures. 67 thus: 68 {{{ 69 integerToMaybeNat :: forall n. NatI n => Integer > Maybe (Nat n) 70 integerToMaybeNat x 71  x == natToInteger (nat :: Nat n) = Just nat 72  otherwise = Nothing 73 }}} 67 74 68 75 Now, we can use `integerToNat` to provide a `Read` instance for singleton types: