Zulip Chat Archive

Stream: new members

Topic: bool=Prop?


view this post on Zulip Thorsten Altenkirch (Oct 23 2020 at 08:50):

Why does this type check?

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

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:51):

#backticks

view this post on Zulip Kenny Lau (Oct 23 2020 at 08:51):

(removed)

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:51):

What are you surprised about?

view this post on Zulip Kenny Lau (Oct 23 2020 at 08:51):

if you #print it you'll see coercions everywhere

view this post on Zulip Johan Commelin (Oct 23 2020 at 08:52):

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

view this post on Zulip Thorsten Altenkirch (Oct 23 2020 at 08:52):

I pressed return prematurely.

view this post on Zulip Thorsten Altenkirch (Oct 23 2020 at 08:53):

So ¬ is overloaded?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 23 2020 at 09:13):

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

view this post on Zulip 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