<div dir="ltr">Hello all,<br><br>I have a question on the `unify` function in Reflection API.<br>I got two minimal examples of multi-step addition of natural numbers (nat.agda, nat-param.agda).<br><br>In the first example (nat.agda), the goal of the fourth argument is dependent on the second argument, but I can unify the desired constructor.<br><br>multi-step : Reduce* (E (V 0) (V 1)) (V 1)<br>multi-step = trans* (E (V 0) (V 1))<br>                    {!!} -- 2nd arg<br>                    (V 1)<br>                    {!runTC!} -- 4th arg, runTC succeeds<br>                    {!!}<br><br>In another example (nat-param.agda), datatype definitions are parameterized, but those parameters don't have any real meanings.<br>When I try the following code, `unify` function in Reflection API fails unless I fill up the second argument.<br><br>multi-step : (v : Typ) → Reduce* v (E (V 0) (V 1)) (V 1) -- we have a parameter `v`<br>multi-step v = trans* (E (V 0) (V 1))<br>                      {!!} -- 2nd arg<br>                      (V 1)<br>                      {!runTC!} -- 4th arg, runTC fails<br>                      {!!}<br><br>I am not sure why this happens, and not sure of any difference between the `unify` function and the refine command in Emacs Mode.<br><br>Any comments would be appreciated.<br><br>Best,<br><br>Chiaki Ishio<br><a href="mailto:chiaki.ishio@gmail.com">chiaki.ishio@gmail.com</a></div>