帰納型から、それが同じコンストラクタから来ているかどうかという関数を自動生成する

[Seasawher]

たとえば Nat.succ 2 と Nat.succ 3 は同じコンストラクタから来ているという意味では同じ。そういう同一視をする関数 Nat → Bool を定義するにはパターンマッチをすれば良いが、では自動生成できるか？

コード例にするとこんな感じ:

inductive EnumLike : Type where
  | foo (name : String)
  | bar (name : String)

def EnumLike.sameKind : EnumLike → EnumLike → Bool
  | EnumLike.foo _, EnumLike.foo _ => true
  | EnumLike.bar _, EnumLike.bar _ => true
  | _, _ => false

[Seasawher]

できれば、属性を自作することにより実現したい。