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):
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