2015-08-12 22:05:14 +00:00
|
|
|
import data.examples.vector
|
2015-05-19 20:09:10 +00:00
|
|
|
open vector
|
|
|
|
|
|
|
|
|
|
set_option pp.implicit true
|
|
|
|
|
|
|
|
|
|
attribute and.rec_on [recursor 4]
|
|
|
|
|
|
|
|
|
|
example (a b : Prop) (h : a ∧ b) : a :=
|
|
|
|
|
begin
|
|
|
|
|
induction h using and.rec_on with ha hb,
|
|
|
|
|
exact ha
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
example (A : Type) (n : nat) (v w : vector A n) (h : v = w) : w = v :=
|
|
|
|
|
begin
|
|
|
|
|
induction v with n a t r,
|
|
|
|
|
rewrite -h,
|
|
|
|
|
rewrite -h
|
|
|
|
|
end
|
