MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "vec_eta.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(pred : Nat) -> < Nat.succ pred : Nat >
term  add : Nat -> Nat -> Nat
{ add Nat.zero y = y
; add (Nat.succ x) y = Nat.succ (add x y)
}
type  Vec : ++(A : Set) -> ^ Nat -> Set
term  Vec.vnil : .[A : Set] -> < Vec.vnil : Vec A Nat.zero >
term  Vec.vcons : .[A : Set] -> ^(head : A) -> .[n : Nat] -> ^(tail : Vec A n) -> < Vec.vcons head n tail : Vec A (Nat.succ n) >
term  head : .[A : Set] -> .[n : Nat] -> (vcons : Vec A (Nat.succ n)) -> A
{ head [A] [n] (Vec.vcons #head [.n] #tail) = #head
}
term  tail : .[A : Set] -> .[n : Nat] -> (vcons : Vec A (Nat.succ n)) -> Vec A n
{ tail [A] [n] (Vec.vcons #head [.n] #tail) = #tail
}
type  Id : ^(A : Set) -> ^(a : A) -> ^ A -> Set
term  Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a a >
error during typechecking:
vec0vnil
/// checkExpr 0 |- \ A -> \ n -> \ v -> \ v' -> refl : .[A : Set] -> (n : Nat) -> (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// checkForced fromList [] |- \ A -> \ n -> \ v -> \ v' -> refl : .[A : Set] -> (n : Nat) -> (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// new A : Set
/// checkExpr 1 |- \ n -> \ v -> \ v' -> refl : (n : Nat) -> (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// checkForced fromList [(A,0)] |- \ n -> \ v -> \ v' -> refl : (n : Nat) -> (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// new n : Nat
/// checkExpr 2 |- \ v -> \ v' -> refl : (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// checkForced fromList [(n,1),(A,0)] |- \ v -> \ v' -> refl : (v : Vec A n) -> (v' : Vec A n) -> Id (Vec A n) v v'
/// new v : (Vec v0 v1)
/// checkExpr 3 |- \ v' -> refl : (v' : Vec A n) -> Id (Vec A n) v v'
/// checkForced fromList [(n,1),(A,0),(v,2)] |- \ v' -> refl : (v' : Vec A n) -> Id (Vec A n) v v'
/// new v' : (Vec v0 v1)
/// checkExpr 4 |- refl : Id (Vec A n) v v'
/// checkForced fromList [(n,1),(A,0),(v,2),(v',3)] |- refl : Id (Vec A n) v v'
/// leqVal' (subtyping)  < Id.refl : Id (Vec A n) v v >  <=+  Id (Vec A n) v v'
/// leqVal' (subtyping)  Id (Vec A n) v v  <=+  Id (Vec A n) v v'
/// leqVal'  v  <=^  v' : Vec A n
/// leqApp: head mismatch v != v'