lean2/tests/lean/unfold_rec.lean.expected.out

unfold_rec.lean:10:2: proof state
n m : ℕ
⊢ succ n + succ m = succ (succ (n + m))
unfold_rec.lean:23:2: proof state
n m : ℕ
⊢ succ (n + succ m) = succ (succ (n + m))
unfold_rec.lean:38:2: proof state
fibgt0 : ∀ b n c, fib ℕ b n c > 0,
b m c : ℕ
⊢ fib ℕ b m c + fib ℕ b (succ m) c > 0
unfold_rec.lean:47:2: proof state
A : Type,
B : Type,
unzip_zip : ∀ {n} v₁ v₂, unzip (zip v₁ v₂) = (v₁, v₂),
m : ℕ,
a : A,
va : vector A m,
b : B,
vb : vector B m
⊢ (a :: prod.pr1 (unzip (zip va vb)), b :: prod.pr2 (unzip (zip va vb))) = (a :: va, b :: vb)
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								unfold_rec.lean:10:2: proof state
-												feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function

See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.

											
										
										
											2015-07-09 01:08:24 +00:00
+								n m : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								⊢ succ n + succ m = succ (succ (n + m))
 								unfold_rec.lean:23:2: proof state
-												feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function

See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.

											
										
										
											2015-07-09 01:08:24 +00:00
+								n m : ℕ
 								⊢ succ (n + succ m) = succ (succ (n + m))
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								unfold_rec.lean:38:2: proof state
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								fibgt0 : ∀ b n c, fib ℕ b n c > 0,
-												feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function

See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.

											
										
										
											2015-07-09 01:08:24 +00:00
+								b m c : ℕ
 								⊢ fib ℕ b m c + fib ℕ b (succ m) c > 0
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								unfold_rec.lean:47:2: proof state
-												feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function

See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.

											
										
										
											2015-07-09 01:08:24 +00:00
+								A : Type,
 								B : Type,
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								unzip_zip : ∀ {n} v₁ v₂, unzip (zip v₁ v₂) = (v₁, v₂),
-												feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function

See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.

											
										
										
											2015-07-09 01:08:24 +00:00
+								m : ℕ,
 								a : A,
 								va : vector A m,
 								b : B,
 								vb : vector B m
 								⊢ (a :: prod.pr1 (unzip (zip va vb)), b :: prod.pr2 (unzip (zip va vb))) = (a :: va, b :: vb)