lean2/tests/lean/run/blast_ematch9.lean

constant P : nat → Prop
definition h [reducible] (n : nat) := n
definition foo [forward] : ∀ x, P (h x) := sorry

set_option blast.ematch true

example (n : nat) : P (h n) :=
by blast
test(tests/lean/run): add Dan's reducible+ematch test 2015-12-03 07:32:13 +00:00			`constant P : nat → Prop`
			`definition h [reducible] (n : nat) := n`
			`definition foo [forward] : ∀ x, P (h x) := sorry`

			`set_option blast.ematch true`

			`example (n : nat) : P (h n) :=`
			`by blast`