coinductive types

Stream: new members

[Thorsten Altenkirch]

Can you define coinductive types in lean? E.g. the conaturals. In Agda:

record ℕ∞ : Set where
  coinductive
  field
    pred∞ : Maybe ℕ∞

[Mario Carneiro]

No, right now any coinductive types have to be hand rolled. The QPF framework can construct arbitrary coinductive types but it's still a work in progress

[Mario Carneiro]

The conaturals are isomophic to mathlib's computation unit, and enat and with_top nat are also classically isomorphic

[Mario Carneiro]

There are no plans to support coinductive types in the lean kernel. It is possible to construct any coinductive type using inductive types, but keep in mind that you don't get the computation rules except as lemmas this way

[Bryan Gin-ge Chen]

This is just word association on my part, but is the "coinductive predicates" file relevant at all here?

[Mario Carneiro]

It is somewhat relevant, depending on how seriously you take propositions as types

[Mario Carneiro]

there are two somewhat distinct things - coinductive types and coinductive predicates, with indexed coinductive types subsuming both