Skip to content

Commit

Permalink
Merge pull request #145 from placidex/typo
Browse files Browse the repository at this point in the history
Fix for typo in custom tactic example
  • Loading branch information
Julian authored Aug 27, 2024
2 parents 4ffaf96 + 8390a98 commit 43b700d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions lean/main/09_tactics.lean
Original file line number Diff line number Diff line change
Expand Up @@ -61,13 +61,13 @@ example : 42 = 42 := by
We can now try a harder problem, that cannot be immediately dispatched by `rfl`:
-/

#check_failure (by custom_tactic : 42 = 4342 = 42)
#check_failure (by custom_tactic : 43 = 4342 = 42)
-- type mismatch
-- Iff.rfl
-- has type
-- ?m.1437 ↔ ?m.1437 : Prop
-- but is expected to have type
-- 42 = 43 ∧ 42 = 42 : Prop
-- 43 = 43 ∧ 42 = 42 : Prop

/-
We extend the `custom_tactic` tactic with a tactic that tries to break `And`
Expand Down

0 comments on commit 43b700d

Please sign in to comment.