declaration contains local constants

Stream: new members

[Horatiu Cheval]

I wasn't able to isolate a mwe so far, but before I try any further I figured it would be better to ask about this in general.
After proving some lemmas I get an failed to add declaration to environment, it contains local constants error. I couldn't find documentation on this. What does this mean? And more importantly what does it entail? I seem to be able to use the lemmas in further proofs with no trouble, as if the error did not exist.

[Alex J. Best]

It's not a common error at all, you can search zulip for the error message and find other examples that arose from people repeating variable names for instance. But without more context its hard to say more. If making an actual MWE is complicated, a MWE of "check out this branch" is easy enough for people try and better than no context for helping :smile:.

[Horatiu Cheval]

Thank you. I figured it out while trying to create the mwe. For future reference, what I did was basically this

section
  parameters (x y z : ℕ)
  parameters (h₁ : x = 0) (h₂ : x = y) (h₃ : y = z)

  include h₁ h₂
  lemma l₁ : y = 0 :=
  begin
    rw [←h₂, h₁],
  end
  omit h₁ h₂

  include h₃
  lemma l₂ : z = 0 :=
  begin
    rw [←h₃, l₁],
  end
  omit h₃
end

For lemma l₂ it appeared to me as if I only needed h₃ and lemma l₁, but in turn l₁ needs h₁ h₂, and the result of not including them in l₂ was my error.

[Horatiu Cheval]

variable would have avoided all this, so I guess the moral is: don't use parameter for hypotheses :)