<div dir="ltr"><div dir="ltr"><div>Use C-c C-;</div><div><br></div><div>(<a href="https://agda.readthedocs.io/en/v2.6.0/tools/emacs-mode.html#commands-in-context-of-a-goal">https://agda.readthedocs.io/en/v2.6.0/tools/emacs-mode.html#commands-in-context-of-a-goal</a>)<div><br></div></div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Apr 21, 2019 at 9:19 AM 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">Aha, I see. Your example also works for me. I tried the following instead<div>...</div><div><div>test : ℕ</div><div>test = {!showGoal!}</div></div><div>...</div><div>so I only got the type of `{! ... !}`. In this case, is it possible to get `ℕ` directly while working inside a hole? </div><div><br></div><div><br></div><div>-- Liang-Ting </div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 21 Apr 2019 at 08:52, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@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>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" target="_blank">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_8891706808323180817gmail-m_-12292170039411437gmail-m_-8463510208427085783gmail-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>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail-m_8891706808323180817gmail-m_-12292170039411437gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div>
</blockquote></div>