Changes between Version 3 and Version 4 of Commentary/Compiler/TypeNatSolver
 Timestamp:
 Dec 9, 2012 5:02:28 PM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Commentary/Compiler/TypeNatSolver
v3 v4 110 110 Rules: 111 111 Add_def(5,3) : 5 + 3 ~ 8 112 Add_fun : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2112 Add_fun : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2 113 113 114 1. Add [W] C: 5 + 3 ~ x to inert set 114 1. Add to inert set: 115 [W] C: 5 + 3 ~ x 115 116 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 118 120 4. Solved: 119 [W] C = Add_def(5,3)121 [W] C = Add_def(5,3) 120 122 }}} 121 123