class inductive?

Stream: lean4

[Yuri de Wit]

I just noticed from one of the earlier comments that there is such a thing as class inductive, but I could not find anything about it in the Lean4 (or 3) manual.

Lean4's source code includes:

class inductive Nonempty (α : Sort u) : Prop where
  | intro (val : α) : Nonempty α

Or

class inductive Decidable (p : Prop) where
  | isFalse (h : Not p) : Decidable p
  | isTrue  (h : p) : Decidable p

I don't really have even an intuition for when should I use a class inductive. In addition, for instance, how is the former class inductive Nonempty different than just a regular class Nonempty with a single method?

[Notification Bot]

Yuri de Wit has marked this topic as resolved.

[Notification Bot]

Yuri de Wit has marked this topic as unresolved.

[Simon Hudon]

class inductive is to class as inductive is to structure. In both cases, the former (i.e. class inductive and inductive) is more expressive than the latter (i.e. class and structure) but the latter gets you some convenience in a special case

[pcpthm]

class inductive ... just expands to @[class] inductive ... like class ... expands to @[class] structure ....
As for Nonempty, because it is defined to be in the universe Prop regardless of the parameter type, it is not possible to define the projection Nonempty α → α without the axiom of choice. structure automatically generates projections, and results in an error.

[Yuri de Wit]

So, I should use class inductive when I am trying to create a class for a Prop?

[Reid Barton]

If the class has non-Prop fields