[Agda] How to obtain the reflected goal?

[Ulf Norell]

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