New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Equation compiler ignores namespace for aux lemma #1841

robertylewis opened this Issue Oct 6, 2017 · 0 comments


None yet
1 participant

robertylewis commented Oct 6, 2017


  • [x ] Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.


In some circumstances, the equation compiler produces lemmas in the root namespace. This causes problems when you import two files which define similar terms in different namespaces. E.g. vector.cons (in the basic library, data/vector.lean) and seq.cons (in mathlib, data/seq/seq/lean) both define cons._main._proof_1, so you can't import both.

Steps to Reproduce

namespace n1
def f : {n : ℕ // n = 0}  {n : ℕ // n = 0}
| ⟨ v, h ⟩ := ⟨ v, h.symm.symm ⟩
end n1

#check @f._main._proof_1 

Expected behavior: [What you expect to happen]

f._main._proof_1 should be named n1.f._main._proof_1

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]
100%. It doesn't seem to happen with all of the aux declarations from the equation compiler though.


3.3.1, master

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment