difference between two forms

Stream: new members

[Iocta]

What is the difference between this one that compiles

example (h : p ∨ q) : q ∨ p :=
or.elim h
  (assume hp : p,
    show q ∨ p, from or.intro_right q hp)
  (assume hq : q,
    show q ∨ p, from or.intro_left p hq)

and this one that doesn't?

example : p ∨ q → q ∨ p :=
or.elim
  (assume hp : p,
    show q ∨ p, from or.intro_right q hp)
  (assume hq : q,
    show q ∨ p, from or.intro_left p hq)

[Mario Carneiro]

there is a missing h on the first line of the proof

[Mario Carneiro]

Your second example is equivalent to this:

example (h : p ∨ q) : q ∨ p :=
or.elim
  (assume hp : p,
    show q ∨ p, from or.intro_right q hp)
  (assume hq : q,
    show q ∨ p, from or.intro_left p hq)
  h

and or.elim takes its arguments in a different order than that

[Iocta]

I don't quite get it. How should it look? I don't see why there should be an h involved at all?

[Joe]

The type of or.elim is a ∨ b → (a → c) → (b → c) → c

[Joe]

So the first argument of or.elim should be something of the type p ∨ q.

[Joe]

But in your second example, the first thing you feed to or.elim is of the type p → q ∨ p.

[Joe]

Here is the way to fix your second example.

example : p ∨ q → q ∨ p :=
λ h,
or.elim h
  (_)
  (_)

[Iocta]

Ah I see. Thanks.