10 lines
325 B
Text
10 lines
325 B
Text
|
[n, m] : list ℕ
|
|||
|
|
[n, i] : list ℤ
|
|||
|
|
[i, n] : list ℤ
|
|||
|
|
[i, n, x] : list ℝ
|
|||
|
|
[i, n, x, y] : vector ℝ 4
|
|||
|
|
tail [i, n, x, y] = v : Prop
|
|||
|
|
[i, n, x] = v : Prop
|
|||
|
|
eq (vector.cons i (vector.cons n (vector.cons x vector.nil))) v : Prop
|
|||
|
|
eq (vector.tail (vector.cons i (vector.cons n (vector.cons x (vector.cons y vector.nil))))) v : Prop
|