From 31159a4d8a4f94349b9c006846518942be798bd0 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 17 Feb 2025 10:24:11 +0900 Subject: [PATCH] doc: paraphrase docstring of `Paradox.spearShield` --- TPIL/Exam/Exam01.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/TPIL/Exam/Exam01.lean b/TPIL/Exam/Exam01.lean index 95eca1f..379745b 100644 --- a/TPIL/Exam/Exam01.lean +++ b/TPIL/Exam/Exam01.lean @@ -108,9 +108,9 @@ infix:55 " can_pierce " => SpearShield.CanPierce variable {Spear : Type u} {Shield : Type u} [SpearShield Spear Shield] -/-- A man trying to sell a spear and a shield claimed that his spear could pierce any shield, and -then claimed that his shield was unpierceable. Then, asked about what would happen if he were to -take his spear to strike his shield, the seller could not answer. -/ +/-- A man trying to sell a spear and a shield claimed that his spear could pierce any shield and +then claimed that his shield could not be pierced. When asked about what would happen if he took his +spear to strike his shield, the seller could not answer. -/ theorem Paradox.spearShield (h₁ : ∃ (spr : Spear), ∀ (shd : Shield), spr can_pierce shd) (h₂ : ∃ (shd : Shield), ∀ (spr : Spear), ¬spr can_pierce shd) : False :=