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: May 02 2025 at 03:31 UTC
Can we make subsingleton types like fintype and decidable behave like proof irrelevance?
Last updated: May 02 2025 at 03:31 UTC