classically unconstructive

Stream: maths

[Sean Leather]

Johan Commelin:

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.