<div dir="ltr"><div dir="ltr"><div>Can you give a complete example? The following works:</div><div><br></div><div><span style="font-family:monospace,monospace">open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)<br>open import Agda.Builtin.Unit<br>open import Agda.Builtin.List<br>open import Agda.Builtin.Nat<br><br>macro<br>  showGoal : Term → TC ⊤<br>  showGoal hole =<br>    inferType hole >>= λ goal → typeError (termErr goal ∷ [])<br><br>test : Nat<br>test = showGoal<br>-- Error:<br>-- Nat<br>-- when checking ...<br></span></div><div><br></div><div>In general if you encounter a meta that you can't handle in a tactic you can call `blockOnMeta`, which causes</div><div>the tactic to be aborted and rerun once the meta is solved.</div><div><br></div><div>/ Ulf<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Apr 20, 2019 at 10:39 PM Liang-Ting Chen <<a href="mailto:liang.ting.chen.tw@gmail.com">liang.ting.chen.tw@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi all, <div><br></div><div>Based on Language Reference, I expect that the following fragment </div><div><br></div></div></div></div></div></div></div><blockquote style="margin:0px 0px 0px 40px;border:medium none;padding:0px"><div><div><div><div><div><div><div><div><font face="monospace, monospace">macro</font></div></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">  showGoal : Term → TC ⊤</font></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">  showGoal hole =</font></div></div></div></div></div></div></div><div><div><div><div><div><div><div><font face="monospace, monospace">    (inferType hole) >>= λ goal → typeError [ termErr goal ]</font></div></div></div></div></div></div></div></blockquote><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>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? </div><div><br></div></div></div></div></div></div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">-- <br><div dir="ltr" class="gmail-m_2901383533489798005gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div></div></div></div></div></div></div></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>