Stream: new members
Topic: tutorials 0019/20
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?
Yakov Pechersky (Jul 10 2020 at 00:44):
modus ponens and
modus ponens, reversed
Sara Fish (Jul 10 2020 at 00:46):
Ah, of course! Thanks.
Heather Macbeth (Jul 10 2020 at 01:12):
That's funny, I always thought
mp was a mnemonic for "implies" :)
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...
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