[Agda] Question on `unify` function in Reflection API

[Ulf Norell]

I get the same behaviour for both nat.agda and nat-param.agda (i.e. runTC
succeeds, but
leaves an unsolved meta for the proof). It might be worth filing an issue
on the bug tracker
with more specifics (agda version, what error are you seeing, etc).

The main difference between unify and Emacs mode refine is that refine
works on the source
code level (so refining with plus_ is roughly equivalent to manually
replacing the hole with `plus ?`
and reloading), whereas unify is working with the internal representations
of the type checker.

/ Ulf

On Fri, Oct 11, 2019 at 9:34 AM 石尾千晶 <chiaki.ishio at gmail.com> wrote:

> Hello all,
>
> I have a question on the `unify` function in Reflection API.
> I got two minimal examples of multi-step addition of natural numbers
> (nat.agda, nat-param.agda).
>
> 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.
>
> multi-step : Reduce* (E (V 0) (V 1)) (V 1)
> multi-step = trans* (E (V 0) (V 1))
>                     {!!} -- 2nd arg
>                     (V 1)
>                     {!runTC!} -- 4th arg, runTC succeeds
>                     {!!}
>
> In another example (nat-param.agda), datatype definitions are
> parameterized, but those parameters don't have any real meanings.
> When I try the following code, `unify` function in Reflection API fails
> unless I fill up the second argument.
>
> multi-step : (v : Typ) → Reduce* v (E (V 0) (V 1)) (V 1) -- we have a
> parameter `v`
> multi-step v = trans* (E (V 0) (V 1))
>                       {!!} -- 2nd arg
>                       (V 1)
>                       {!runTC!} -- 4th arg, runTC fails
>                       {!!}
>
> I am not sure why this happens, and not sure of any difference between the
> `unify` function and the refine command in Emacs Mode.
>
> Any comments would be appreciated.
>
> Best,
>
> Chiaki Ishio
> chiaki.ishio at gmail.com
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191016/b473fe9f/attachment.html>