## Stream: new members

### Topic: coinductive types

#### Thorsten Altenkirch (Sep 25 2020 at 14:42):

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

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


#### Mario Carneiro (Sep 25 2020 at 14:48):

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 (Sep 25 2020 at 14:51):

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

#### Mario Carneiro (Sep 25 2020 at 14:53):

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 (Sep 25 2020 at 14:57):

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

#### Mario Carneiro (Sep 25 2020 at 14:58):

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

#### Mario Carneiro (Sep 25 2020 at 14:59):

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

Last updated: May 15 2021 at 00:39 UTC