feat: abbrev produces theorems where appropriate

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

feat: abbrev produces theorems where appropriate #6083

Open kim-em opened 1 week ago

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-14 23:35:49)
✅ Mathlib branch lean-pr-testing-6083 has successfully built against this PR. (2024-11-21 08:55:45) View Log

eric-wieser commented 1 week ago

Is there any advantage of using abbrev over theorem in this case?

kim-em commented 1 week ago

Is there any advantage of using abbrev over theorem in this case?

Yes, we can use abbrev X := @Y, to avoid having the type out the signature, when deprecating. In Batteries and below, we have alias, but I don't think alias is ready to move upstream (precisely because it results in us having too many ways to do the same thing: eventually I would like a unification of abbrev and alias functionality into a single keyword).