Skip to content

Commit

Permalink
Merge pull request #728 from lean-ja/Seasawher/issue619
Browse files Browse the repository at this point in the history
simp at * が通らず simp_all が通る例
  • Loading branch information
Seasawher authored Aug 30, 2024
2 parents ae0adb1 + 09f7921 commit e44fa93
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion Examples/Tactic/Simp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,12 @@ example {x y : Nat} : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
simp_arith

/- ## simp_all
`simp_all` は `simp [*] at *` の強化版で、ローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/
`simp_all` はローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/

example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ (Q ∧ (P → Q)) := by
-- simp at * は失敗する
fail_if_success simp at *

simp_all

end Simp --#

0 comments on commit e44fa93

Please sign in to comment.