<div dir="ltr"><div dir="ltr"><div>Dear Ulf,</div><div><br></div><div>Thank you so much for the reply here and on GitHub.<br></div><br>(I created a new issue on GitHub: <a href="https://github.com/agda/agda/issues/4143" target="_blank">https://github.com/agda/agda/issues/4143</a>)</div><div><br></div><div><br></div><div>Chiaki Ishio</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">2019年10月16日(水) 23:03 Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>I get the same behaviour for both nat.agda and nat-param.agda (i.e. runTC succeeds, but</div><div> leaves an unsolved meta for the proof). It might be worth filing an issue on the bug tracker</div><div>with more specifics (agda version, what error are you seeing, etc).</div><div><br></div><div>The main difference between unify and Emacs mode refine is that refine works on the source</div><div>code level (so refining with plus_ is roughly equivalent to manually replacing the hole with `plus ?`</div><div> and reloading), whereas unify is working with the internal representations of the type checker.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Oct 11, 2019 at 9:34 AM 石尾千晶 <<a href="mailto:chiaki.ishio@gmail.com" target="_blank">chiaki.ishio@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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" target="_blank">chiaki.ishio@gmail.com</a></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr">Chiaki Ishio<br><a href="mailto:chiaki.ishio@gmail.com" target="_blank">chiaki.ishio@gmail.com</a></div></div>