lean: The `a` bug
Prerequisites
- 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.
- Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn’t already filed.
Description
The famous a bug doesn’t need a description, we have all met it.
Steps to Reproduce
example (a : ℕ) : true :=
begin
have : ∀ n, n ≥ 0 → a ≤ a,
sorry
end
Expected behavior: [What you expect to happen]
No error.
Actual behavior: [What actually happens]
Lean chooses the name a for the premise n ≥ 0 and confuses itself.
Reproduces how often: [What percentage of the time does it reproduce?]
100%
Versions
Lean (version 3.18.4, commit f539be1e867c, Release)
About this issue
- Original URL
- State: closed
- Created 4 years ago
- Reactions: 1
- Comments: 17 (17 by maintainers)
Commits related to this issue
- fix(frontends/lean/builtin_exprs): "fix" "`a` bug" In tactic mode, `p -> a` would be interpreted as `Π (a : p), a`, capturing the variable `a`. Change the binder name used by `->` to `_x` to avoid th... — committed to rwbarton/lean-1 by rwbarton 4 years ago
- fix(frontends/lean/builtin_exprs): "fix" "`a` bug" (#490) In tactic mode, `p -> a` would be interpreted as `Π (a : p), a`, capturing the variable `a`. Change the binder name used by `->` to `ᾰ` to ... — committed to leanprover-community/lean by gebner 4 years ago
I suggest
_xinstead, which is already used as the base name for\lam _, ...binders. I don’t see a good reason to have a separate naming system for arrow variables.Can we do 1 character? If it’s going to be shorter than _x it has to be 1 character. Keep in mind that this will be extensively prefixed, you can get things like
h_⚠️_1_1_2_⚠️_3if the base name is⚠️My vote is still for
_x. I would like to keep the length of autogenerated names down, because I’m sure I will see it 50 times per medium sized tactic state. Seeingfixmescrawled all over my tactic state obscuring the actual content, sounds like a bad idea.What about a funny unicode character? That can keep the visible size down while also making it hard to type, which should help to discourage explicit use in proofs.
So…
deadbeef?I edited my earlier comment to use
_xand to expand the list of visible side effects. PR is #442.