search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.69k stars 421 forks source link

RFC: Deprecate `admit` #4901

Open adomasbaliuka opened 3 months ago

adomasbaliuka commented 3 months ago

Proposal

Currently, admit and sorry are synonyms.

If we deprecate the one that is less used, which is admit, beginners have one less thing to worry about what it does and if there's subtle differences to sorry.

Community Feedback

Deprecation suggested in this discussion after a beginner asked if there is a difference.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

Kha commented 3 months ago

The motivation here is not very strong, "one less thing to worry about" doesn't strike us as significant given the large number of tactics Lean already comes with. On the other hand, users coming from other ITPs may benefit from this familiar name. While this RFC does come with quite a few +1's, we would have to hear from more specific voices like educators to consider accepting this change.