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