michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/run): define vector diagonal using recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-04 17:57:25 -08:00
parent 7488378445
commit 7ff03e2846
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/lean/run/eq7.lean Normal file
View file

@ -0,0 +1,13 @@
import data.vector
open nat vector
definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n,
diag nil := nil,
diag ((a :: va) :: vs) := a :: diag (map tail vs)
theorem diag_nil (A : Type) : diag (@nil (vector A 0)) = nil :=
rfl
theorem diag_succ {A : Type} {n : nat} (a : A) (va : vector A n) (vs : vector (vector A (succ n)) n) :
diag ((a :: va) :: vs) = a :: diag (map tail vs) :=
rfl