What functions are generated for inductive type?

Stream: new members

[Kevin Cheung]

Is there a way to list all the automatically generated functions for an inductive type?

I know there is .rec, .casesOn, and .recOn. Are there others?

[Kevin Buzzard]

You could try writing whatsnew in before the definition of the type.

import Mathlib.Tactic

whatsnew in
inductive MyNat
/-
def MyNat._sizeOf_1 : MyNat → ℕ :=
fun t ↦ MyNat.rec (fun t ↦ ℕ) t

protected def MyNat.noConfusion.{u} : {P : Sort u} → {v1 v2 : MyNat} → v1 = v2 → MyNat.noConfusionType P v1 v2 :=
fun {P} {v1 v2} h12 ↦
  Eq.ndrec (motive := fun a ↦ v1 = a → MyNat.noConfusionType P v1 a)
    (fun h11 ↦ MyNat.casesOn (fun {v1} ↦ MyNat.noConfusionType P v1 v1) v1) h12 h12

protected def MyNat.casesOn.{u} : (motive : MyNat → Sort u) → (t : MyNat) → motive t :=
fun motive t ↦ MyNat.rec motive t

def MyNat._sizeOf_inst : SizeOf MyNat :=
{ sizeOf := fun m ↦ m._sizeOf_1 }

protected def MyNat.noConfusionType.{u} : Sort u → MyNat → MyNat → Sort u :=
fun P v1 v2 ↦ MyNat.casesOn (fun v1 ↦ Sort u) v1

recursor MyNat.rec.{u} : (motive : MyNat → Sort u) → (t : MyNat) → motive t

inductive MyNat : Type
constructors:

protected def MyNat.recOn.{u} : (motive : MyNat → Sort u) → (t : MyNat) → motive t :=
fun motive t ↦ MyNat.rec motive t
-/

[Kevin Cheung]

I see. But what if the type is already defined?

[Riccardo Brasca]

As a workaround you can copy/paste the definition in your file (changing the name) and see what whatsnew says. I don't know if there is a better way. (You can of course modify the file where definition is written, but at the beginning it is better to not modify mathlib).

[Matthew Ballard]

What does autocomplete expose?

[Kevin Cheung]

Thanks.

[Kevin Cheung]

Screenshot-2024-07-08-at-12.02.09PM.png

[Kevin Cheung]

What is toCtorIdx?

[Matthew Ballard]

It is generated here and indexes the constructors via natural numbers

Eg

inductive Weekday : Type :=
  | Mon : Weekday
  | Tue : Weekday
  | Wed : Weekday
  | Thu : Weekday
  | Fri : Weekday
  | Sat : Weekday
  | Sun : Weekday

#eval Weekday.toCtorIdx .Mon -- 0
#eval Weekday.toCtorIdx .Tue -- 1
#eval Weekday.toCtorIdx .Wed -- 2
#eval Weekday.toCtorIdx .Thu -- 3
#eval Weekday.toCtorIdx .Fri -- 4
#eval Weekday.toCtorIdx .Sat -- 5
#eval Weekday.toCtorIdx .Sun -- 6

[Kevin Cheung]

Thank you.