unknown identifier 'h'

Stream: new members

[David Renshaw]

I expect this to work:

section

variables (a b : ℕ) (h : a < b)

lemma foo : a < b :=
begin
  exact h,
end

end

but I get:

error: unknown identifier 'h'

What's going wrong here? Am I not allowed to use variables like that?

[Bryan Gin-ge Chen]

Lean doesn't include hypotheses from variables unless they appear in the type. You can use include h to force Lean to include the variable in all following declarations.

[David Renshaw]

aha! Thanks.

[Bryan Gin-ge Chen]

This is discussed briefly about halfway through TPiL 5.1.

[David Renshaw]

Yep, I remember reading that a while ago, but I apparently didn't retain it.

[Alex Zhang]

In my case, why does Lean give me the error message unknown identifier 'h' and unknown identifier 'g'?

import data.nat.prime
open nat

-- BEGIN
example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) :
  m ∣ n ∧ ¬ n ∣ m :=
⟨ h.1,  λ g, by absurd (dvd_antisymm (h.1) g) h.2 ⟩
-- END

[Sebastien Gouezel]

You should remove the by, since absurd is a lemma you are applying, not a tactic.

[Alex Zhang]

I didn't notice that before. Thanks a lot!!