# Changes between Version 57 and Version 58 of TypeFunctionsSolving

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

--

Unmodified
Removed
Modified
• ## TypeFunctionsSolving

 v57 == Propagation (aka Solving) == A significant difference to new-single is that solving is a purely local operation.  We never instantiate any flexible variables. A significant difference to `new-single` is that solving is a purely local operation.  We never instantiate any flexible variables. === Rules === '''Top''':: {{{ co :: F t1..tn ~ t =(Top)=> co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co' }}} where `g :: forall x1..xm. F u1..um ~ s` and `[s1/x1, .., sm/xm]u1 == t1`. '''!SubstFam''':: {{{ co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s =(SubstFam)=> co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' }}} where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. '''!SubstVarVar''':: {{{ co1 :: x ~ t  &  co2 :: x ~ s =(SubstVar)=> co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' }}} where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. '''!SubstVarFam''':: {{{ }}} '''TODO:'''