@[match_pattern] 属性を紹介する

Examples/Command/Attribute/MatchPattern.lean

@@ -0,0 +1,30 @@
+/- # match_pattern
+
+`match_pattern` 属性を付与すると、元々コンストラクタしか使用できない `match` 式でのパターンマッチの枝に、指定した関数を使うことができるようになります。
+-/
+
+/-- 自前で定義したリスト -/
+inductive MyList (α : Type) where
+  | nil : MyList α
+  | cons : α → MyList α → MyList α
+
+variable {α : Type}
+
+/-- MyList の `cons` コンストラクタに対するラッパー。中身は同じ -/
+def MyList.myCons (a : α) (as : MyList α) : MyList α :=
+  MyList.cons a as
+
+-- 最初は `match` の中で `MyList.myCons` を使うことはできない
+/-- error: invalid pattern, constructor or constant marked with '[match_pattern]' expected -/
+#guard_msgs in
+  def badLength : MyList α → Nat
+    | MyList.nil => 0
+    | MyList.myCons _ as => 1 + badLength as
+
+-- `match_pattern` 属性を付与する
+attribute [match_pattern] MyList.myCons
+
+-- これで `match` の中で `MyList.myCons` を使うことができる
+def goodLength : MyList α → Nat
+  | MyList.nil => 0
+  | MyList.myCons _ as => 1 + goodLength as

src/SUMMARY.md

@@ -64,6 +64,7 @@
     - [csimp: 効率的な実装に置換](./Command/Attribute/Csimp.md)
     - [induction_eliminator: 独自帰納法](./Command/Attribute/InductionEliminator.md)
     - [inherit_doc: ドキュメントの継承](./Command/Attribute/InheritDoc.md)
+    - [match_pattern: 独自パタンマッチ](./Command/Attribute/MatchPattern.md)
     - [simps: simp補題の自動生成](./Command/Attribute/Simps.md)
 
 - [タクティク](./Tactic/README.md)