Skip to content

Commit

Permalink
fix typo in variable declaration in example
Browse files Browse the repository at this point in the history
I noticed this while learning lean through the documentation. 
The declaration of `tp` seems like a typo to me.
  • Loading branch information
Swiftb0y authored and leodemoura committed Nov 17, 2022
1 parent a92c32b commit 19f4757
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion propositions_and_proofs.md
Original file line number Diff line number Diff line change
Expand Up @@ -607,7 +607,7 @@ contradiction. This rule is sometimes called *ex falso* (short for *ex
falso sequitur quodlibet*), or the *principle of explosion*.

```lean
variable (tp q : Prop)
variable (p q : Prop)
example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)
```
Expand Down

0 comments on commit 19f4757

Please sign in to comment.