Changes between Version 57 and Version 58 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 10:46:15 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v57 v58  
    134134== Propagation (aka Solving) ==
    135135
    136 A significant difference to new-single is that solving is a purely local operation.  We never instantiate any flexible variables.
     136A significant difference to `new-single` is that solving is a purely local operation.  We never instantiate any flexible variables.
     137
     138=== Rules ===
     139
     140 '''Top'''::
     141{{{
     142co :: F t1..tn ~ t
     143=(Top)=>
     144co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co' 
     145}}}
     146 where `g :: forall x1..xm. F u1..um ~ s` and `[s1/x1, .., sm/xm]u1 == t1`.
     147
     148 '''!SubstFam'''::
     149{{{
     150co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
     151=(SubstFam)=>
     152co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
     153}}}
     154 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.
     155
     156 '''!SubstVarVar'''::
     157{{{
     158co1 :: x ~ t  &  co2 :: x ~ s
     159=(SubstVar)=>
     160co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'
     161}}}
     162 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.
     163
     164 '''!SubstVarFam'''::
     165{{{
     166}}}
    137167
    138168'''TODO:'''