Codata and Recursion scheme in Lean

Stream: lean4

[Erika Su]

Hi, I am a newbie for lean language. I have some question to which i cannot find answer simply by google. Hopefully someone can help me.
First, recursion scheme and codata: A common pattern for functional language is

(co)inductive Fix (f : Type -> Type) : Type :=
  | f (Fix f)

which define how a data can be constructed (the maximum fixpoint in term of domain theory).
If we use inductive in the above definiton, the lean would correctly reject the program, as pattern matching on such data structure cannot assure termination.
So, how shall i apply codata pattern in term of programming in lean? Shall i just define a typeclass describing how data can be destructed?

[James Gallicchio]

as far as I'm aware there's not good support yet for co-inductive types :/ I believe someone was working on porting QPF to Lean 4, but I don't think it's ready for general use yet

relevant: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Coinduction.3F