From 8ba78272f4b579cd2c6ad07c04cb6cf208d174d7 Mon Sep 17 00:00:00 2001 From: ia0 Date: Thu, 16 Jul 2026 12:15:28 +0200 Subject: [PATCH] doc: mention left and right to prove disjunction The structure of the sentence follows the one for conjunction in the previous section. --- Manual/BasicProps.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/BasicProps.lean b/Manual/BasicProps.lean index 1ab21d99a..42d24bd19 100644 --- a/Manual/BasicProps.lean +++ b/Manual/BasicProps.lean @@ -112,7 +112,7 @@ Because {lean}`Sum` is a type, it is possible to check _which_ constructor was u {lean}`Or`, on the other hand, forms propositions: terms that prove a disjunction cannot be interrogated to check which disjunct was true. In other words, because {lean}`Or` is not a {tech}[subsingleton], its proofs cannot be used as part of a computation. -In a {ref "tactics"}[tactic] proof, disjunctions can be proved using either constructor ({name}`Or.inl` or {name}`Or.inr`) explicitly via {tactic}`apply`. +In a {ref "tactics"}[tactic] proof, disjunctions can be proved using either constructor ({name}`Or.inl` or {name}`Or.inr`) explicitly via {tactic}`apply`, but {tactic}`left` and {tactic}`right` are more common. Assumptions of disjunctions in the context can be simplified using {tactic}`cases`, pattern matching with {tactic (show := "match")}`Lean.Parser.Tactic.match`, or {tactic}`rcases`. {docstring Or}