Zulip Chat Archive

Stream: new members

Topic: coinductive types


view this post on Zulip 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 

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 25 2020 at 14:58):

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

view this post on Zulip 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