<div dir="ltr">I don't understand, "pruning" means looking at metavariables and their substitutions on the right hand side of an equation, and removing dependencies on out-of-scope variables; see the example Ulf wrote before. Variables inside the substitution on the left hand side of an equation aren't targets of pruning in any way.<br></div><div class="gmail_extra"><br><div class="gmail_quote">2016-11-28 8:49 GMT+01:00 Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I wonder, why prune when you can just solve? Consider the flexRigid case<br>
<br>
U [vs] =?= t<br>
<br>
where `vs` is a list of variables (not necessarily different). We<br>
traverse `t` and check whether<br>
<br>
1) each variable in `t` occurs at least ones in `vs`. If not so,<br>
then throw a "can't unify" error.<br>
2) each variable in `t` occurs exactly ones in `vs`.<br>
2.1) If so, we have a solution. I.e. this equation:<br>
<br>
U [x, y, w, w] =?= App (Var x) (Var y)<br>
<br>
gets solved by<br>
<br>
U [x, y, _, _] := App (Var x) (Var y)<br>
<br>
without any explicit pruning.<br>
2.2) If not so, then we can prune sometimes. E.g.<br>
<br>
U [x, y, w, w] =?= App (Var x) (Var w)<br>
<br>
results in pruning of `y` if the type of `w` doesn't depend on it.<br>
<br>
Does this sound right?<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>