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


Ignore:
Timestamp:
Dec 9, 2012 5:08:18 PM (3 years 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