<div dir="ltr">Oops, there are surprisingly many typos in my previous email. Hope it is still understandable. <div><br></div><div>Anyway, I forgot to mention that the above code is tested with the development version of Agda on GitHub.  -- Liang-Ting </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 30 May 2019 at 13:41, 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-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi all, <div><br></div><div>I found that the de Bruijn indices in the context extended by `extendContext` does not corresponds to the right position in the context. For example, in the following metaprogram, the indices of the argument `a` and the argument in the extended context are both `0` as executing `λ x → test x` shows `0 0`. Shouldn't the index for `a` be 1? </div><div><br></div><div><div><div><font face="courier new, monospace">macro</font></div><div><font face="courier new, monospace">  test : ℕ → Term → TC ⊤</font></div><div><font face="courier new, monospace">  test a _ = do</font></div><div><font face="courier new, monospace">    extendContext (vArg (quoteTerm ℕ)) do</font></div><div><font face="courier new, monospace">      (var₀ i , var₀ j) ← ⦇ (quoteTC =<< unquoteTC {A = ℕ} (var₀ 0)) , quoteTC a ⦈ </font></div><div><font face="courier new, monospace">        where _ → {!!}</font></div><div><font face="courier new, monospace">      typeError (strErr (show i) ∷ (strErr (show j)) ∷ [])</font></div></div><div><br></div><div><br></div>-- <br><div dir="ltr" class="gmail-m_-5521101266585895345gmail_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>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div>