騎士と悪党のパズルの説明文を修正

帰納型にすることが悪いわけではない
lean-ja · Aug 20, 2024 · e9d00d4 · e9d00d4
1 parent 41ebbe3
commit e9d00d4
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 12 deletions.
diff --git a/Examples/Exercise/KnightAndKnave.lean b/Examples/Exercise/KnightAndKnave.lean
@@ -56,12 +56,6 @@ axiom knight_ne_knave (p : Islander) : ¬(knight p ∧ knave p)
     intro h
     simp_all
 
-/-
-```admonish warning title="注意"
-`Islander` 型を `knight` と `knave` の２つのコンストラクタを持つ帰納型として定義すると、島民が２人しかいないことになってしまって、正しい表現にならないことに注意して下さい。
-```
--/
-
 /- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/
 
 /-- ゾーイ -/

diff --git a/Examples/Solution/KnightAndKnave.lean b/Examples/Solution/KnightAndKnave.lean
@@ -56,12 +56,6 @@ axiom knight_ne_knave (p : Islander) : ¬(knight p ∧ knave p)
     intro h
     simp_all
 
-/-
-```admonish warning title="注意"
-`Islander` 型を `knight` と `knave` の２つのコンストラクタを持つ帰納型として定義すると、島民が２人しかいないことになってしまって、正しい表現にならないことに注意して下さい。
-```
--/
-
 /- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/
 
 /-- ゾーイ -/