diff --git a/LeanByExample/Parser/AnonymousConstructor.lean b/LeanByExample/Parser/AnonymousConstructor.lean index da0c8687..2f144ce9 100644 --- a/LeanByExample/Parser/AnonymousConstructor.lean +++ b/LeanByExample/Parser/AnonymousConstructor.lean @@ -56,7 +56,7 @@ structure Hoge where -- 両者は同じものを表している! x = y -/- 上の例は構造体の同種のコンストラクタが入れ子になっている例ですが、構造体でも同種のコンストラクタでもなくても平坦化することができます。 -/ +/- 上の例は構造体の同種のコンストラクタが入れ子になっている例ですが、`structure` コマンドで定義された型でなくても、同種のコンストラクタでもなくても、同様に平坦化することができます。 -/ /-- Prod を真似て自作した帰納型 -/ inductive MyProd (α β : Type) where