<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_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>