class inductive

Stream: general

[Mario Carneiro]

Check out the definition of nonempty:

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

Even the syntax highlighter didn't know class inductive was a thing

[Mario Carneiro]

not zulip's highlighter but I think it doesn't understand definition structure

[Mario Carneiro]

(Personally I don't think it should be a thing, since @[class] inductive works just as well)

[Jireh Loreaux]

what are some useful examples of @[class] inductive?

[Frédéric Dupuis]

I guess you could imagine something like

@[class] inductive IsROrC (𝕜 : Type _) [Field 𝕜]
| real (e : 𝕜 ≃+* ℝ)
| complex (e : 𝕜 ≃+* ℂ)

[Eric Wieser]

I think we used to have more of these, but we eliminated them in favor of using structures containing more primitive inductive types as fields

[Henrik Böving]

The most useful one by far is of course docs4#Decidable !

[Eric Wieser]

Off-topic, but is it easy to fix the docs for that so that the docstrings for the constructors are not monospaced?

[Henrik Böving]

That should be a simple :tm: CSS fix yes

[Henrik Böving]

Should be fixed on the next build

[Jireh Loreaux]

@Frédéric Dupuis that's actually exactly the application I was considering!

[Kevin Buzzard]

[insert my canonical moan about how it shouldn't be Is because it's not a Prop]

[Henrik Böving]

Eric Wieser said:

Off-topic, but is it easy to fix the docs for that so that the docstrings for the constructors are not monospaced?

better?^^

[Notification Bot]

14 messages were moved from this topic to #general > inductive types in documentation by Kyle Miller.