匿名コンストラクタという言葉の指す対象が間違っていたので修正

Src/Anonymous.lean

@@ -1,29 +1,30 @@
 /- # 匿名コンストラクタ
-匿名コンストラクタは，帰納型(構造体も含まれます) `T` に対して `T` 型の項を分解（デコンストラクト）する方法のひとつです．
+匿名コンストラクタは，構造体 `T` に対して `T` 型の項を構成する方法のひとつです．
 
-これは以下に示すように，`⟨x1, x2, ...⟩ | ⟨y1, y2, ...⟩ | ..` という構文により使うことができます．
+これは以下に示すように，`⟨x1, x2, ...⟩` という構文により使うことができます．
 -/
 set_option linter.unusedVariables false --#
 
-inductive Sample where
-  | fst (foo bar : Nat) : Sample
-  | snd (foo bar : Int) : Sample
+/-- 2つのフィールドを持つ構造体 -/
+structure Hoge where
+  foo : Nat
+  bar : Nat
+
+def hoge : Hoge := ⟨1, 2⟩
 
-theorem sample_triv (s : Sample) : True := by
-  obtain ⟨f1, b1⟩ | ⟨f2, b2⟩ := s
+/- コンストラクタが入れ子になっていても平坦化することができます．例えば，以下の2つの定義は同じことをしています．-/
 
-  case fst =>
-    trivial
+def foo : Nat × (Int × String) := ⟨1, ⟨2, "foo"⟩⟩
 
-  case snd =>
-    trivial
+def foo' : Nat × Int × String := ⟨1, 2, "foo"⟩
 
-/- 匿名コンストラクタを使用しない場合，次のようにコンストラクタ名を指定する必要があります．-/
+/- 一般の帰納型に対しては使用できません．-/
 
-theorem sample_triv' (s : Sample) : True := by
-  cases s with
+inductive Sample where
+  | fst (foo bar : Nat) : Sample
+  | snd (foo bar : String) : Sample
 
-  | fst f b =>
-    trivial
-  | snd f b =>
-    trivial
+-- invalid constructor ⟨...⟩,
+-- expected type must be an inductive type with only one constructor
+--   Sample
+#check_failure (⟨"foo", "bar"⟩ : Sample)