or.elim unknown identifier

Stream: general

[Bernd Losert]

I have this piece of code:

  le_conv := begin
    intros y l₁' l₂' h₀ h₁,
    or.elim h₁ _ _
  end,

For some reason, the first error that I get from this is error: unknown identifier 'h₁'. I don't understand why though since h₁ is right there. Help!

[Yaël Dillies]

or.elim isn't a tactic but a term. Try refine or.elim h₁ _ _ instead.

[Bernd Losert]

Works. Good to know. Thanks.