Zulip Chat Archive

Stream: lean4

Topic: class inductive?


Yuri de Wit (Jul 20 2022 at 01:24):

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 (Jul 20 2022 at 01:24):

Yuri de Wit has marked this topic as resolved.

Notification Bot (Jul 20 2022 at 01:24):

Yuri de Wit has marked this topic as unresolved.

Simon Hudon (Jul 20 2022 at 01:29):

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 (Jul 20 2022 at 08:19):

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 (Jul 20 2022 at 16:43):

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

Reid Barton (Jul 20 2022 at 17:05):

If the class has non-Prop fields


Last updated: Dec 20 2023 at 11:08 UTC