1
{-# OPTIONS -v tc.conv.irr:50 #-}
2
module IndexInference where
8
data Vec (A : Set) : Nat -> Set where
10
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
14
foo : Vec Nat _ -> Nat
15
foo (a :: b :: c :: []) = c
29
data Fin (n : Nat) : Set where
30
zero : .(NonZero n) → Fin n
31
suc : .(NonZero n) → Fin (pred n) → Fin n
33
data SubVec (A : Set)(n : Nat) : Fin n → Set where
34
[] : .{p : NonZero n} → SubVec A n (zero p)
35
_::_ : .{p : NonZero n}{k : Fin (pred n)} → A → SubVec A (pred n) k → SubVec A n (suc p k)
37
bar : {A : Set} → SubVec A (suc (suc (suc zero))) _ → A