lean2/tests/lean/run/rewriter12.lean

import data.nat
open nat algebra
constant f : nat → nat

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, add_zero at H1, H1]

example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, add_zero at H1, H1]
feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 19:03:36 +00:00			`import data.nat`
refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading 2015-10-14 19:27:09 +00:00			`open nat algebra`
feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 19:03:36 +00:00			`constant f : nat → nat`

			`example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=`
fix(tests/lean/run): adjust some tests to changes in the standard library 2015-10-13 22:39:03 +00:00			`by rewrite [▸* at H1, add_zero at H1, H1]`
feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 19:03:36 +00:00
			`example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=`
fix(tests/lean/run): adjust some tests to changes in the standard library 2015-10-13 22:39:03 +00:00			`by rewrite [▸* at H1, add_zero at H1, H1]`