Skip to content

Instantly share code, notes, and snippets.

@luxbock

luxbock/lean_hmm.lean

Created August 27, 2018 19:10
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/981f990d263516589146ffeb3825e421 to your computer and use it in GitHub Desktop.
Save luxbock/981f990d263516589146ffeb3825e421 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
lean_hmm.lean
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
(assume h, _)
/-
propositions_as_types.lean:432:13: error
don't know how to synthesize placeholder
context:
p q r : Prop,
h : p ∨ q → r
⊢ (p → r) ∧ (q → r)
-/
(assume (h : (p → r) ∧ (q → r))
(hpq : p ∨ q),
have pir : (p → r), from h.left,
have qir : (q → r), from h.right,
show r, from
or.elim hpq
(assume hp, pir hp)
(assume hq, qir hq))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment