[Agda] extendContext in reflection

[Liang-Ting Chen]

Hi all,

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?

macro
  test : ℕ → Term → TC ⊤
  test a _ = do
    extendContext (vArg (quoteTerm ℕ)) do
      (var₀ i , var₀ j) ← ⦇ (quoteTC =<< unquoteTC {A = ℕ} (var₀ 0)) ,
quoteTC a ⦈
        where _ → {!!}
      typeError (strErr (show i) ∷ (strErr (show j)) ∷ [])


-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190530/b824c559/attachment.html>