Zulip Chat Archive

Stream: new members

Topic: TPIL Chap 3 exercise help


view this post on Zulip Luca Seemungal (Aug 30 2019 at 16:06):

Hi, the following

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
(assume h : p ∧ (q ∨ r),
    or.elim h.right,
    (assume hq : q,
      or.inl (and.intro h.left hq))
    (assume hr : r,
      or.inr (and.intro h.left hr)))
(assume h : (p ∧ q) ∨ (p ∧ r), sorry)

gives me errors at h.left, with unknown identifier h.left

But I get h.left from the assume h : p ∧ (q ∨ r) line! What is the issue here? This is all module the sorry, obviously. Thanks!

view this post on Zulip Koundinya Vajjha (Aug 30 2019 at 16:28):

Get rid of the comma after h.right


Last updated: May 11 2021 at 00:31 UTC