Changes between Version 2 and Version 3 of TypeNats/MatchingOnNats
 Timestamp:
 Sep 23, 2012 4:01:00 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/MatchingOnNats
v2 v3 86 86 by the following two rules: 87 87 {{{ 88 forall a b. (FromNat1 a ~ FromNat1 b) => (a ~ b)89 forall a. exists b. (1 <= FromNat1 a) => (a ~ Succ b)88 forall a b. (FromNat1 a ~ FromNat1 b) => (a ~ b) 89 forall a. exists b. (1 <= FromNat1 a) => (a ~ Succ b) 90 90 }}} 91 91 92 92 93 Now the function `getField` typechecks as expected: 94 {{{ 95 s :: Selector 2 93 96 97 p :: Ptr (Struct [Int,Char,Float]) 98 99 f :: Ptr Float 100 f = getField s p 101 }}} 102