Zulip Chat Archive
Stream: general
Topic: matching subsingletons
Kenny Lau (Sep 10 2018 at 10:09):
Can we make subsingleton types like fintype and decidable behave like proof irrelevance?
Last updated: Dec 20 2023 at 11:08 UTC
Can we make subsingleton types like fintype and decidable behave like proof irrelevance?
Last updated: Dec 20 2023 at 11:08 UTC