[Agda] How to obtain the reflected goal?

[Liang-Ting Chen]

It works. Thank you so much! -- Liang-Ting

On Sun, 21 Apr 2019 at 09:36, Ulf Norell <ulf.norell at gmail.com> wrote:

> Use C-c C-;
>
> (
> https://agda.readthedocs.io/en/v2.6.0/tools/emacs-mode.html#commands-in-context-of-a-goal
> )
>
> / Ulf
>
> On Sun, Apr 21, 2019 at 9:19 AM Liang-Ting Chen <
> liang.ting.chen.tw at gmail.com> wrote:
>
>> Aha, I see. Your example also works for me. I tried the following instead
>> ...
>> test : ℕ
>> test = {!showGoal!}
>> ...
>> so I only got the type of `{! ... !}`. In this case, is it possible to
>> get `ℕ` directly while working inside a hole?
>>
>>
>> -- Liang-Ting
>>
>> On Sun, 21 Apr 2019 at 08:52, Ulf Norell <ulf.norell at gmail.com> wrote:
>>
>>> Can you give a complete example? The following works:
>>>
>>> open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
>>> open import Agda.Builtin.Unit
>>> open import Agda.Builtin.List
>>> open import Agda.Builtin.Nat
>>>
>>> macro
>>>   showGoal : Term → TC ⊤
>>>   showGoal hole =
>>>     inferType hole >>= λ goal → typeError (termErr goal ∷ [])
>>>
>>> test : Nat
>>> test = showGoal
>>> -- Error:
>>> -- Nat
>>> -- when checking ...
>>>
>>> In general if you encounter a meta that you can't handle in a tactic you
>>> can call `blockOnMeta`, which causes
>>> the tactic to be aborted and rerun once the meta is solved.
>>>
>>> / Ulf
>>>
>>> On Sat, Apr 20, 2019 at 10:39 PM Liang-Ting Chen <
>>> liang.ting.chen.tw at gmail.com> wrote:
>>>
>>>> Hi all,
>>>>
>>>> Based on Language Reference, I expect that the following fragment
>>>>
>>>> macro
>>>>   showGoal : Term → TC ⊤
>>>>   showGoal hole =
>>>>     (inferType hole) >>= λ goal → typeError [ termErr goal ]
>>>>
>>>>
>>>> binds the reflected goal to `goal`, but I always get a meta-variable
>>>> instead even if the goal is simply ℕ. Is this the expected behaviour?
>>>>
>>>> --
>>>> Best regards,
>>>> Liang-Ting
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>
>>
>> --
>> Best regards,
>> Liang-Ting
>>
>

-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190421/6b88545e/attachment.html>