Non-struct classes are not supported

[dselsam]

Mathlib uses this idiom many times:

@[class] def ...

In Lean4, only structures can be classes. The porting tool ignores such class annotations. Ideally, Mathlib backports this restriction.

[dselsam]

Apparently, for many of the use-cases in Mathlib, the definitions reduce to structure classes, e.g.

def has_finite_products : Prop :=
Π (J : Type v) [decidable_eq J] [fintype J], has_limits_of_shape (discrete J) C

attribute [class] has_finite_products

instance has_limits_of_shape_discrete
  (J : Type v) [fintype J] [has_finite_products C] :
  has_limits_of_shape (discrete J) C :=
by { classical, exact ‹has_finite_products C› J }

Thus if they were actually reducible they wouldn't need this annotation. The comment above has_finite_products claims it cannot be made reducible due to https://github.com/leanprover-community/lean/issues/429 though I don't grok the connection yet. Perhaps these can just be made reducible in Lean4 during the auto-porting.

Also, right now Lean4 requires that all TC subgoals reduce to a class without reducing anything semireducible (https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/SynthInstance.lean#L189-L193) though perhaps it would be acceptable to reduce here at TransparencyMode.default since we know we are looking for a class and must fail otherwise.

[digama0]

@dselsam Does @[class] inductive or class inductive work? There is exactly one instance of such a thing in mathlib.

[dselsam]

Yes:

class inductive Foo (n : Nat) : Type
| mk : Fin n → Foo n

def foo {n : Nat} [foo : Foo n] : Fin n :=
  match foo with
  | Foo.mk i => i

instance fooInst : Foo 5 := Foo.mk ⟨4, sorry⟩
def test : Fin 5 := foo

set_option pp.all true in
#print test
/-
def test : Fin (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)) :=
@foo (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)) fooInst
-/

[dselsam]

@[class] inductive Foo also works.