Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
You can’t perform that action at this time.