diff --git a/Examples/Command/Attribute/MatchPattern.lean b/Examples/Command/Attribute/MatchPattern.lean new file mode 100644 index 00000000..8e7aeb49 --- /dev/null +++ b/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 diff --git a/src/SUMMARY.md b/src/SUMMARY.md index b7121765..119a7a45 100644 --- a/src/SUMMARY.md +++ b/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)