Skip to content

Commit

Permalink
doc: contradiction docstring indendation (#5470)
Browse files Browse the repository at this point in the history
Just saw some bad markdown, thought I’ll quickly fix it.
  • Loading branch information
nomeata authored Sep 25, 2024
1 parent 3e2a465 commit 78c40f3
Showing 1 changed file with 16 additions and 15 deletions.
31 changes: 16 additions & 15 deletions src/Init/Tactics.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 78c40f3

Please sign in to comment.