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


Ignore:
Timestamp:
Dec 9, 2012 5:02:28 PM (2 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