-
-
Save luxbock/f0c19afd8d88fef9c13814ba072b9eb5 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Internally, the expression have h : p, from s, t produces the | |
-- term (λ (h : p), t) s. In other words, s is a proof of p, t is | |
-- a proof of the desired conclusion assuming h : p, and the two | |
-- are combined by a lambda abstraction and application. | |
example (h : p ∧ q) : q ∧ p := | |
have hp : p, from and.left h, | |
have hq : q, from and.right h, | |
show q ∧ p, from and.intro hq hp | |
example (h : p ∧ q) : q ∧ p := | |
(λ hp : p, | |
(λ hq : q, | |
and.intro hp hq) | |
and.right h) | |
and.left h | |
/- | |
propositions_as_types.lean:690:1: error | |
type mismatch at application | |
(λ (hp : p), ⁇) and.left | |
term | |
and.left | |
has type | |
?m_1 ∧ ?m_2 → ?m_1 | |
but is expected to have type | |
p | |
propositions_as_types.lean:691:3: error | |
type mismatch at application | |
(λ (hq : q), ⟨hp, hq⟩) and.right | |
term | |
and.right | |
has type | |
?m_1 ∧ ?m_2 → ?m_2 | |
but is expected to have type | |
q | |
-/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment