Stream: Hydras & Co. universe

Topic: Library for countability?

view this post on Zulip Lessness (Mar 14 2023 at 20:03):

In the theories/ordinals/Schutte/Countable.v file of hydra-battles, there is an ad-hoc formalization of countable Prop-based sets. The question is "is there already such a formalization in the Coq libraries ?"

(from PM by Pierre Castéran)

Is this task important/good right now? If yes, I'm going to take a look at this file and then explore if there's some library that does the same job...

Last updated: Jun 10 2023 at 23:01 UTC