## Stream: new members

### Topic: bool=Prop?

#### Thorsten Altenkirch (Oct 23 2020 at 08:50):

Why does this type check?

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


#backticks

(removed)

#### Kenny Lau (Oct 23 2020 at 08:51):

if you #print it you'll see coercions everywhere

#### Johan Commelin (Oct 23 2020 at 08:52):

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

#### Thorsten Altenkirch (Oct 23 2020 at 08:52):

I pressed return prematurely.

#### Thorsten Altenkirch (Oct 23 2020 at 08:53):

So ¬ is overloaded?

#### Reid Barton (Oct 23 2020 at 08:54):

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 (Oct 23 2020 at 08:59):

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 (Oct 23 2020 at 09:13):

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

#### Chris B (Oct 23 2020 at 11:12):

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


Last updated: May 10 2021 at 23:11 UTC