Non-structure `class`es

Stream: general

[Eric Wieser]

Did we decide that one or both of these was outlawed in mathlib (for lean 4 reasons?)

class inductive has_foo_ind (A : Type*)
| strong_foo (h : ∃ x : ℤ, true) : has_foo_ind
| weak_foo (h : ∃ x : ℕ, true) : has_foo_ind

@[class]
def has_foo_def (A : Type*) := (∃ x : ℤ, true) ∨ (∃ x : ℕ, true)

[Gabriel Ebner]

The second one is definitely out.

[Gabriel Ebner]

Class inductives should be fine though (I hope).

[Eric Wieser]

Alright, good; I was thinking of suggesting using class inductive in #6671, as it seems to make the or easier to work with:

import algebra.char_p.basic
import algebra.char_zero
import data.nat.prime

/-- The definition of the exponential characteristic of a semiring. (from the PR) -/
class exp_char (R : Type*) [semiring R] (q : ℕ) : Prop :=
(exp_char_def : (q = 1 ∧ char_zero R) ∨ (q.prime ∧ char_p R q))

/-- Easier definition to work with? -/
class inductive exp_char' (R : Type*) [semiring R] (q : ℕ) : Prop
| zero (hq : q = 1) [char_zero R] : exp_char'
| prime (hq : q.prime) [char_p R q] : exp_char'

variables (R : Type*) [integral_domain R]

example [hq : exp_char' R 3] : true := begin
  casesI hq,  -- unpacks all the instances
  sorry,
  sorry,
end

example [hq : exp_char R 3] : true := begin
  cases hq.exp_char_def,  -- requires unpacking ands
  { haveI := h.2,
    sorry},
  { haveI := h.2,
    sorry}
end

[Eric Wieser]

cc @Jakob Scholbach