Skip to content

Instantly share code, notes, and snippets.

@luxbock
Created September 2, 2018 19:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save luxbock/f0c19afd8d88fef9c13814ba072b9eb5 to your computer and use it in GitHub Desktop.
Save luxbock/f0c19afd8d88fef9c13814ba072b9eb5 to your computer and use it in GitHub Desktop.
-- 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