[Agda] How to obtain the reflected goal?

[Liang-Ting Chen]

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/dec1699f/attachment.html>