Changes between Version 2 and Version 3 of TypeNats/MatchingOnNats


Ignore:
Timestamp:
Sep 23, 2012 4:01:00 AM (3 years 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