diff --git a/Examples/Exercise/KnightAndKnave.lean b/Examples/Exercise/KnightAndKnave.lean index 7ca3e5bf..d8dc8408 100644 --- 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` の2つのコンストラクタを持つ帰納型として定義すると、島民が2人しかいないことになってしまって、正しい表現にならないことに注意して下さい。 -``` --/ - /- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/ /-- ゾーイ -/ diff --git a/Examples/Solution/KnightAndKnave.lean b/Examples/Solution/KnightAndKnave.lean index 0685cbda..d7410f5e 100644 --- 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` の2つのコンストラクタを持つ帰納型として定義すると、島民が2人しかいないことになってしまって、正しい表現にならないことに注意して下さい。 -``` --/ - /- これでゾーイとメルが島民であり、騎士か悪党かのどちらかであるということは次のように表現できます。-/ /-- ゾーイ -/