[Agda] extendContext in reflection

[Liang-Ting Chen]

Oops, there are surprisingly many typos in my previous email. Hope it is
still understandable.

Anyway, I forgot to mention that the above code is tested with the
development version of Agda on GitHub.  -- Liang-Ting

On Thu, 30 May 2019 at 13:41, Liang-Ting Chen <liang.ting.chen.tw at gmail.com>
wrote:

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


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