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

refactor(library/data/vector): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-03 21:06:17 -08:00
parent 173e84c299
commit 7d19b5b743
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/vector.lean
View file

@ -54,9 +54,7 @@ namespace vector
rfl rfl
theorem eta (v : vector A (succ n)) : head v :: tail v = v := theorem eta (v : vector A (succ n)) : head v :: tail v = v :=
-- TODO(Leo): replace 'head_cons h t ▸ tail_cons h t ▸ rfl' with rfl destruct v (λ n h t, rfl)
-- after issue #318 is fixed
destruct v (λ n h t, head_cons h t ▸ tail_cons h t ▸ rfl)
definition last : vector A (succ n) → A := definition last : vector A (succ n) → A :=
nat.rec_on n nat.rec_on n