Is there codata in lean? What about non-terminating IO?

Stream: general

[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:
图片.png
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?

Another problem is IO that cannot ensure termination:
图片.png
the manual says lean4 doesn't have meta yet. So how do i implement this intention?