1
{-# OPTIONS --sized-types #-}
5
open import Common.Size
9
{-# BUILTIN SIZELT Size< #-}
14
data T (i : Size) : Set where
15
c : (j : Size< i) → T j → T _
18
bug i (c j x) = bug j x
20
{- WAS: de Bruijn index out of scope
22
Issue700.bug is projection like in argument 1 for type Issue700.T
24
delta = (j : Size< @0) (x : T j)
26
ps = [r(ConP Issue700.T.c Nothing [r(VarP "j"),r(VarP "x")])]
27
body = Bind (Abs "h1" Bind (Abs "h2" Body (Def Issue700.bug [r(Var 1 []),r(Var 0 [])])))
28
body = [h1 h2] bug h1 h2