Huajian Xin (Oct 13 2022 at 11:56):
For extract tactic information in metaprogramming environment I need to transfer some codes from term mode to tactic mode, but it seem to be non-trivial for some inductive proofs. For example, in
data.int.basic there is a theorem
theorem div_neg : ∀ (a b : ℤ), a / -b = -(a / b) | (m : ℕ) 0 := show of_nat (m / 0) = -(m / 0 : ℕ), by rw nat.div_zero; refl | (m : ℕ) (n+1:ℕ) := rfl | 0 -[1+ n] := by simp | (m+1:ℕ) -[1+ n] := (neg_neg _).symm | -[1+ m] 0 := rfl | -[1+ m] (n+1:ℕ) := rfl | -[1+ m] -[1+ n] := rfl
However, the straight transfer seems not work:
Could anyone help me with this problem? Thanks!
Yaël Dillies (Oct 13 2022 at 12:20):
The syntax is (annoyingly) different. You need to insert commas between different arguments in each match.
Huajian Xin (Oct 13 2022 at 12:25):
Thanks! I got it!
Scott Morrison (Oct 13 2022 at 13:34):
This has become uniform in Lean4.
Last updated: Aug 03 2023 at 10:10 UTC