From 78c40f380c8c40bac58f41fffeea007b357c514d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 25 Sep 2024 11:50:21 +0200 Subject: [PATCH] doc: `contradiction` docstring indendation (#5470) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Just saw some bad markdown, thought I’ll quickly fix it. --- src/Init/Tactics.lean | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 57ed1572df82..3f12057e4ede 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -149,26 +149,27 @@ syntax (name := assumption) "assumption" : tactic /-- `contradiction` closes the main goal if its hypotheses are "trivially contradictory". + - Inductive type/family with no applicable constructors -```lean -example (h : False) : p := by contradiction -``` + ```lean + example (h : False) : p := by contradiction + ``` - Injectivity of constructors -```lean -example (h : none = some true) : p := by contradiction -- -``` + ```lean + example (h : none = some true) : p := by contradiction -- + ``` - Decidable false proposition -```lean -example (h : 2 + 2 = 3) : p := by contradiction -``` + ```lean + example (h : 2 + 2 = 3) : p := by contradiction + ``` - Contradictory hypotheses -```lean -example (h : p) (h' : ¬ p) : q := by contradiction -``` + ```lean + example (h : p) (h' : ¬ p) : q := by contradiction + ``` - Other simple contradictions such as -```lean -example (x : Nat) (h : x ≠ x) : p := by contradiction -``` + ```lean + example (x : Nat) (h : x ≠ x) : p := by contradiction + ``` -/ syntax (name := contradiction) "contradiction" : tactic