Changes between Version 3 and Version 4 of Commentary/Compiler/TypeNatSolver


Ignore:
Timestamp:
Dec 9, 2012 5:02:28 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeNatSolver

    v3 v4  
    110110    Rules:
    111111    Add_def(5,3) : 5 + 3 ~ 8
    112     Add_fun : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2
     112    Add_fun      : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2
    113113
    114     1. Add [W] C: 5 + 3 ~ x to inert set
     114    1. Add to inert set:
     115       [W] C: 5 + 3 ~ x
    115116    2. Generate new derived:
    116      [D] Add_fun(C,Add_def) : x ~ 8   (proof discarded)
    117     3. GHC uses this hint to improve the wanted to [W] C: 5 + 3 ~ 8
     117       [D] Add_fun(C,Add_def) : x ~ 8   (proof discarded)
     118    3. GHC uses this hint to improve and reconsider the wanted:
     119       [W] C: 5 + 3 ~ 8
    118120    4. Solved:
    119      [W] C = Add_def(5,3)
     121       [W] C = Add_def(5,3)
    120122}}}
    121123