From 8390a9811a3fe75f46ef69c6c2e48a998c5c3e06 Mon Sep 17 00:00:00 2001 From: Krishna Padmasola Date: Tue, 27 Aug 2024 11:37:06 +0530 Subject: [PATCH] Fix for typo in custom tactic example --- lean/main/09_tactics.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean index 2a8f990..a02134b 100644 --- a/lean/main/09_tactics.lean +++ b/lean/main/09_tactics.lean @@ -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 = 43 ∧ 42 = 42) +#check_failure (by custom_tactic : 43 = 43 ∧ 42 = 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`