how to use type class within its definition

Stream: lean4

[Locria Cyber]

I was trying to compile the following code, when I realized that I can't use PrunableSemilatticeSup within itself.

import Mathlib.Order.Lattice
import Mathlib.Order.Basic

def larger [PartialOrder α] (a : α) (s : Set α) := ∃ b ∈ s, a ≥ b

class PrunableSemilatticeSup (α : Type u) extends SemilatticeSup α where
  PrunedType : Set α -> Type u
  preserve_prune : (s : Set α) -> PrunableSemilatticeSup (PrunedType s)
  prune : (s : Set α) -> α -> Option (PrunedType s)
  -- prune is correct
  correct : (s : Set α) -> ∀ a: α, larger a s → (prune s a).isSome = true
  -- preserve partial morphology
  preserve : ∀ a b: α, (l : larger a s ∧ larger b s) → prune s (a ⊔ b) = (prune s a).get (correct s a l.left) ⊔ (prune s b).get (correct s b l.right)

How do I get around this limitation?

[Jovan Gerbscheid]

If you want to use an inductive data type, and you want to make it a class, you can use class inductive instead of class. But I'm not sure that's actually what you want here.