From cc76c462449167040906b3c87929aeb765ac0a0a Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Thu, 13 Feb 2025 22:21:18 +0900 Subject: [PATCH] doc: fix typo (#7067) --- src/Init/Classical.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 16db2812f3..08a09802b7 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -195,7 +195,7 @@ end Classical /- Export for Mathlib compat. -/ export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp) -/-- Extract an element from a existential statement, using `Classical.choose`. -/ +/-- Extract an element from an existential statement, using `Classical.choose`. -/ -- This enables projection notation. @[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P