Topic: classically unconstructive
Sean Leather (Jul 18 2018 at 06:09):
I wish that thing (
classical.prop_decidable) would be on by default. People should explicitly state that they want to be constructive if they want to... not vice versa!
Noooo! That would be unconstructive.
Last updated: May 14 2021 at 18:28 UTC