inr

Stream: new members

[Iocta]

What is the difference between

example : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.intro_left _ (and.right z))
  (λ z, or.intro_right _ (and.right z))
)

which compiles and

example : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

which doesn't?

[Kenny Lau]

(deleted)

[Kenny Lau]

(deleted)

[Kenny Lau]

they both compile for me

[Kenny Lau]

variables {p q r : Prop}

example : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.intro_left _ (and.right z))
  (λ z, or.intro_right _ (and.right z))
)

example : (p ∧ q) ∨ (p ∧ r) → q ∨ r :=
(assume h: (p ∧ q) ∨ (p ∧ r),
  show q ∨ r,
  from or.elim h
  (λ z, or.inl  (and.right z))
  (λ z, or.inr (and.right z))
)

[Kenny Lau]

assuming you didn't forget variables {p q r : Prop}

[Iocta]

Oh. they both work for me now too. it just took a while for flycheck to get updated. :-)