Zulip Chat Archive

Stream: new members

Topic: tutorials 0019/20


view this post on Zulip Sara Fish (Jul 10 2020 at 00:39):

In the text right between 0019 and 0020 in this tutorial (https://github.com/leanprover-community/tutorials), they write

Similarly, given a proof h of P ↔ Q, one can get a proof of P → Q using h.mp
and a proof of Q → P using h.mpr

What do mp and mpr stand for?

view this post on Zulip Yakov Pechersky (Jul 10 2020 at 00:44):

modus ponens and modus ponens, reversed

view this post on Zulip Sara Fish (Jul 10 2020 at 00:46):

Ah, of course! Thanks.

view this post on Zulip Heather Macbeth (Jul 10 2020 at 01:12):

That's funny, I always thought mp was a mnemonic for "implies" :)

view this post on Zulip Johan Commelin (Jul 10 2020 at 02:44):

It's true that I don't think I've ever had this terminology used in any of the courses I took...

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 14:08):

But you took very few if any logic courses, right?


Last updated: May 16 2021 at 05:21 UTC