bool=Prop?

Stream: new members

[Thorsten Altenkirch]

Why does this type check?

def bnotz : bool -> bool
| x := ¬x

[Johan Commelin]

#backticks

[Kenny Lau]

(removed)

[Johan Commelin]

What are you surprised about?

[Kenny Lau]

if you #print it you'll see coercions everywhere

[Johan Commelin]

Aha, you are surprised because of the \not instead of !.

[Thorsten Altenkirch]

I pressed return prematurely.

[Thorsten Altenkirch]

So ¬ is overloaded?

[Reid Barton]

It's not overloaded, but there is a coercion from bool to Prop, as well as a coercion from decidable Props back to bool, and a decidable instance for ¬ (b : Prop) for b : bool

[Thorsten Altenkirch]

Thank you. This confused at least one of my students (and me). Sometimes it would be nice to have a student mode that switches off all the clever stuff.

[Kevin Buzzard]

The up-arrows are the clue I guess. I well remember being totally confused by them :-)

[Chris B]

Thorsten Altenkirch said:

Sometimes it would be nice to have a student mode that switches off all the clever stuff.

set_option pp.all true will at least show you everything that's going on under the hood. The printer options stack, so if you want everything but universes you can do

set_option pp.all true
set_option pp.universes off