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

[Chiaki Ishio]

Dear Ulf,

Thank you so much for the reply here and on GitHub.

(I created a new issue on GitHub: https://github.com/agda/agda/issues/4143)


Chiaki Ishio

2019年10月16日(水) 23:03 Ulf Norell <ulf.norell at gmail.com>:

> 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
>>
>

-- 
Chiaki Ishio
chiaki.ishio at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191019/a463d1bc/attachment.html>