Zulip Chat Archive

Stream: general

Topic: Are all inductive types enumerable?


Kenny Lau (Aug 01 2018 at 06:51):

Are all inductive types enumerable?

Mario Carneiro (Aug 01 2018 at 06:54):

inductive types whose parts are enumerable are enumerable

Mario Carneiro (Aug 01 2018 at 06:55):

indeed it's not unreasonable to have a derive_handler for that

Kenny Lau (Aug 01 2018 at 06:55):

it would solve Q4 of my questions lol

Kenny Lau (Aug 01 2018 at 06:56):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/Lean.20assignment.20from.20Kenny/near/130567187

Mario Carneiro (Aug 01 2018 at 06:56):

You can prove finite trees are enumerable by using denumerable (list A) recursively


Last updated: Dec 20 2023 at 11:08 UTC