Coinduction in mathlib4?

Stream: general

[Jihoon Hyun]

What's the status of coinduction support in Lean4? I just got curious while looking at Rocq codes.

[Henrik Böving]

There is support upcoming for coinductive predicates: https://github.com/leanprover/lean4/pull/10333, coindunctive data is not natively supported but there are encodings that make it possible: https://github.com/alexkeizer/QpfTypes

[Violeta Hernández]

In particular, we have docs#QPF.Fix and docs#QPF.Cofix for creating inductive/coinductive types from a docs#QPF (read, some functor that encodes the constructors of the type)