[Agda] How to obtain the reflected goal?

[Ulf Norell]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190421/99f3be84/attachment.html>