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


Ignore:
Timestamp:
Dec 9, 2012 5:08:18 PM (17 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeNatSolver

    v4 v5  
    9999 
    100100``Derived`` constraints are facts that are implied by the constraints 
    101 in the inert set.  They do not have complete proofs because their 
     101in the inert set.  They do not have complete proofs because 
    102102they may depend on proofs of as yet unsolved wanted constraints. 
    103103GHC does not associate any proof terms with derived constraints (to keep things simple?). 
     
    122122}}} 
    123123 
     124The type-nat solver processes derived constraints in a similar fashion 
     125to given constraints:   it checks to see if they are trivially known 
     126and, if not, then it tries to generate some additional derived constraints. 
     127The main difference is that derived constraints can be interacted 
     128with all existing constraints to produce new facts, while given 
     129constraints only interact with other givens. 
    124130 
    125131 
     
    130136 
    131137 
    132  
    133  
    134  
    135  
    136  
    137  
    138