term mode replacement for cases

Stream: new members

[Jakob Scholbach]

Is there a term-mode equivalent of cases? Such as in the following example (the lemma bla is of course useless, just meant to provide a mwe)

variables h1 : Prop
variables h2 : Prop
variables h3 : Prop

lemma bla : h1 ∨ h2 :=
begin sorry end

lemma blub (h1 h2 : Prop): h3 :=
begin
  cases bla h1 h2 with e f, -- this is what I want to replace by term-mode
  { sorry },
  { sorry }
end

[Patrick Massot]

Sure, you can use the recursor directly.

[Jakob Scholbach]

Just omit begin end ?

[Patrick Massot]

Also remember that show_term answers all these questions in principle.

[Kevin Buzzard]

Use or.rec or or.elim or whatever it's called

[Mario Carneiro]

match is also a term mode construct

[Patrick Massot]

lemma blub (h1 h2 : Prop): h3 :=
begin
show_term {  cases bla h1 h2 with e f, -- this is what I want to replace by term-mode
  { sorry },
  { sorry } }
end

[Mario Carneiro]

lemma blub (h1 h2 : Prop): h3 :=
(bla h1 h2).elim
  (λ e, sorry)
  (λ f, sorry)

[Mario Carneiro]

lemma blub (h1 h2 : Prop): h3 :=
match bla h1 h2 with
| or.inl e := sorry
| or.inr f := sorry
end