diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 416c69bbfa..477e55e6cc 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -224,7 +224,7 @@ the first matching constructor, or else fails. syntax (name := constructor) "constructor" : tactic /-- -Applies the second constructor when +Applies the first constructor when the goal is an inductive type with exactly two constructors, or fails otherwise. ``` example : True ∨ False := by