MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "VectorPatternNotForced.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : 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.nil : .[A : Set] -> < Vec.nil : Vec A Nat.zero >
term  Vec.cons : .[A : Set] -> .[n : Nat] -> ^(y1 : A) -> ^(y2 : Vec A n) -> < Vec.cons n y1 y2 : Vec A (Nat.succ n) >
term  length : .[A : Set] -> .[n : Nat] -> Vec A n -> < n : Nat >
{ length [A] [.Nat.zero] Vec.nil = Nat.zero
; length [A] [.(succ n)] (Vec.cons [n] a v) = Nat.succ (length [A] [n] v)
}
term  head : .[A : Set] -> .[n : Nat] -> Vec A (Nat.succ n) -> A
{ head [A] [.n] (Vec.cons [n] a v) = a
}
term  tail : .[A : Set] -> .[n : Nat] -> Vec A (Nat.succ n) -> Vec A n
{ tail [A] [.n] (Vec.cons [n] a v) = v
}
term  zeroes : (n : Nat) -> Vec Nat n
{ zeroes Nat.zero = Vec.nil
; zeroes (Nat.succ x) = Vec.cons [x] Nat.zero (zeroes x)
}
type  Fin : ^ Nat -> Set
term  Fin.fzero : .[n : Nat] -> < Fin.fzero n : Fin (Nat.succ n) >
term  Fin.fsucc : .[n : Nat] -> ^(y1 : Fin n) -> < Fin.fsucc n y1 : Fin (Nat.succ n) >
term  lookup : .[A : Set] -> .[n : Nat] -> Vec A n -> Fin n -> A
{ lookup [A] [.(succ n)] (Vec.cons [n] a v) (Fin.fzero [.n]) = a
; lookup [A] [.(succ n)] (Vec.cons [n] a v) (Fin.fsucc [.n] i) = lookup [A] [n] v i
; lookup [A] [.Nat.zero] Vec.nil ()
}
term  downFrom : .[n : Nat] -> Vec Nat n
error during typechecking:
downFrom
/// clause 1
/// pattern zero
/// checkPattern: constructor Nat.zero of non-computational argument zero : Nat not forced