generate code to detect same constructor

Stream: Is there code for X?

[Asei Inoue]

When defining an inductive type, is it possible to automatically generate a ‘function to determine if the terms of that inductive type come from the same constructor’?

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

[Kyle Miller]

It's possible to write code to generate such a function, but it's unlikely to be something that Lean 4 would do for you.

What's the application?

[Asei Inoue]

my curiosity.

[Asei Inoue]

When I was defining enum-like inductive types, I thought this pattern might appear frequently and was curious if it could be generated automatically.

[Asei Inoue]

It would be nice if this could be achieved by giving the attribute [enum] to the inductive type.

[Kyle Miller]

A true enum is a type whose constructors each have no arguments. In that case, you can use deriving DecidableEq.

inductive Kind where
  | foo | bar
  deriving DecidableEq

inductive EnumLike : Type where
  | mk (kind : Kind) (name : String)

def EnumLike.kind : EnumLike → Kind
  | mk kind _ => kind

def EnumLike.sameKind (a b : EnumLike) : Bool :=
  a.kind = b.kind

[Asei Inoue]

A true enum is a type whose constructors each have no arguments.

my interest is "auto generation of code", not enum