Changes between Version 2 and Version 3 of TypeNats/MatchingOnNats

Show
Ignore:
Timestamp:
09/22/12 21:01:00 (8 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeNats/MatchingOnNats

    v2 v3  
    8686by the following two rules: 
    8787{{{ 
    88 forall a b. (FromNat1 a ~ FromNat1 b) => (a ~ b) 
    89 forall a. exists b. (1 <= FromNat1 a) => (a ~ Succ b) 
     88forall a b.         (FromNat1 a ~ FromNat1 b) => (a ~ b) 
     89forall a. exists b. (1 <= FromNat1 a)         => (a ~ Succ b) 
    9090}}} 
    9191 
    9292 
     93Now the function `getField` type-checks as expected: 
     94{{{ 
     95s :: Selector 2 
    9396 
     97p :: Ptr (Struct [Int,Char,Float]) 
     98 
     99f :: Ptr Float 
     100f = getField s p 
     101}}} 
     102