lean2/tests/lean/interactive/consume_args.input

VISIT consume_args.lean
SYNC 7
import logic data.nat.basic
open nat eq.ops algebra

theorem tst (a b c : nat) : a + b + c = a + c + b :=
calc a + b + c = a + (b + c) : by rewrite add.assoc
         ...   = a + (c + b) : by rewrite (add.comm b c)
         ...   = a + c + b   : by rewrite add.assoc
WAIT
INFO 7
fix(frontends/lean/elaborator): missing type information when `!` operator (aka consume_args) is used 2014-10-20 08:31:16 -07:00			`VISIT consume_args.lean`
			`SYNC 7`
			`import logic data.nat.basic`
refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading 2015-10-14 12:27:09 -07:00			`open nat eq.ops algebra`
fix(frontends/lean/elaborator): missing type information when `!` operator (aka consume_args) is used 2014-10-20 08:31:16 -07:00
			`theorem tst (a b c : nat) : a + b + c = a + c + b :=`
feat(library/blast/forward): inst_simp should use the left-hand-side as a pattern (if none is provided by the user) The motivation is to reduce the number of instances generated by ematching. For example, given inv_inv: forall a, (a⁻¹)⁻¹ = a the new heuristic uses ((a⁻¹)⁻¹) as the pattern. This matches the intuition that inv_inv should be used a simplification rule. The default pattern inference procedure would use (a⁻¹). This is bad because it generates an infinite chain of instances whenever there is a term (a⁻¹) in the proof state. By using (a⁻¹), we get (a⁻¹)⁻¹ = a Now that we have (a⁻¹)⁻¹, we can match again and generate ((a⁻¹)⁻¹)⁻¹ = a⁻¹ and so on 2015-12-31 20:20:39 -08:00			`calc a + b + c = a + (b + c) : by rewrite add.assoc`
			`... = a + (c + b) : by rewrite (add.comm b c)`
			`... = a + c + b : by rewrite add.assoc`
fix(frontends/lean/elaborator): missing type information when `!` operator (aka consume_args) is used 2014-10-20 08:31:16 -07:00			`WAIT`
			`INFO 7`