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

[石尾千晶]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191011/4fc066da/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: nat.agda
Type: application/octet-stream
Size: 1419 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191011/4fc066da/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: nat-param.agda
Type: application/octet-stream
Size: 1630 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191011/4fc066da/attachment-0001.obj>