Iterating over constructors of non-recursive inductive

Stream: new members

[Ioannis Konstantoulas]

Let's say I have a simple inductive type like the following:

inductive Shopping where
  | eggs
  | bread
  | milk

Is there an automatic way to enumerate and get a list of (strings representing) the constructors that gets updated if I decide to add or remove constructors from the type? In other words:

def ShoppingList  : List String := sorry
def NumberOfItems : Nat         := sorry

where the sorry do not need to be modified if I change the contents of Shopping.

[Henrik Böving]

you can do that with meta programming in principle but why would you want this?

[Kyle Miller]

Why not? :smile:

import Lean

section
open Lean Elab Term

elab "constr_list%" n:ident : term => do
  let n ← resolveGlobalConstNoOverloadWithInfo n
  let ival ← getConstInfoInduct n
  -- Assuming every constructor name is a `Name.str`:
  return toExpr (ival.ctors.map Name.getString!)

elab "constr_count%" n:ident : term => do
  let n ← resolveGlobalConstNoOverloadWithInfo n
  let ival ← getConstInfoInduct n
  return toExpr ival.numCtors

end

inductive Shopping where
  | eggs
  | bread
  | milk

def ShoppingList  : List String := constr_list% Shopping
def NumberOfItems : Nat         := constr_count% Shopping

#eval ShoppingList
-- ["eggs", "bread", "milk"]
#eval NumberOfItems
-- 3

[Ioannis Konstantoulas]

Henrik Böving said:

you can do that with meta programming in principle but why would you want this?

I want to encode e.g. actions a program can take in such a finite type. If, later, I want to add or remove an action, I want to have to modify as few parts as possible. I also want these for ad hoc debugging, because I don't yet understand attributes and options (I cannot find much documentation about them, either).

[Kyle Miller]

The Mathlib Fintype derive handler generates a List of all the constructors for an enumeration like this by the way. This isn't documented (yet).