Zulip Chat Archive
Stream: lean4
Topic: Dropping 'admit'
Mario Carneiro (Jul 22 2022 at 03:51):
The sorry term/tactic is used overwhelmingly in favor of admit (which is a tactic but not a term) in mathlib, to the point that I would expect most newcomers to not know that admit exists at all. The admit tactic is also not highlighted in red like sorry (in some static highlighting schemes; the semantic highlighter currently overrides both sorry and admit tactics to the blue keyword color). The admit tactic is a holdover from the Coq tactic of the same name, but we have tended toward more uniformity between term and tactic mode and I propose we drop admit altogether. Downstream users can of course reimplement it using
macro "admit" : tactic => `(sorry)
example : False := by admit -- this is red in prettier but not in vscode AFAIK
if desired.
Mario Carneiro (Jul 22 2022 at 04:44):
This may or may not also extend to dropping the word "admit" in code function names and comments like admitGoal "admits the goal"
Siddhartha Gadgil (Jul 22 2022 at 06:38):
Mario Carneiro said:
This may or may not also extend to dropping the word "admit" in code function names and comments like
admitGoal"admits the goal"
sorryGoal and "sorries the goal" sound ugly (not a serious reason).
Gabriel Ebner (Jul 22 2022 at 07:08):
We could say "excuses the goal". (not 100% serious)
Mac (Jul 22 2022 at 07:16):
Alternatively, one could do the opposite and rename sorry to admit (as it sounds better in things like admitGoal). :wink:
Mario Carneiro (Jul 22 2022 at 07:31):
Yes, I noticed that admit works better as a verb than sorry, although it's also a very weird usage of the word. Colloquially it sounds like an incomplete version of "admit the goal... is hard"
Mario Carneiro (Jul 22 2022 at 07:32):
the boring version would be closeGoalBySorry
Gabriel Ebner (Jul 22 2022 at 07:33):
the semantic highlighter currently overrides both sorry and admit tactics to the blue keyword color
For me sorry is red in vscode. (Never cared about admit so it doesn't have any special highlighting.)
Johan Commelin (Jul 22 2022 at 07:35):
I've given plenty of talks for people who have never seen Lean before. They all seem to think that sorry is hilarious (in a good way!).
Johan Commelin (Jul 22 2022 at 07:36):
If we need an alternative, I suggest IgiveUp.
Mario Carneiro (Jul 22 2022 at 07:39):
Gabriel Ebner said:
the semantic highlighter currently overrides both sorry and admit tactics to the blue keyword color
For me
sorryis red in vscode. (Never cared aboutadmitso it doesn't have any special highlighting.)
You should upstream your local changes then!
Mario Carneiro (Jul 22 2022 at 07:39):
The Coq word for sorry is admit and the Isabelle version is oops
Gabriel Ebner (Jul 22 2022 at 07:40):
You should upstream your local changes then!
I'm not sure I understand you. I get the red sorry with the vanilla extension.
Mario Carneiro (Jul 22 2022 at 07:40):
oh, I thought you had a fancy .vscode settings file to override something or other
Mario Carneiro (Jul 22 2022 at 07:41):
maybe my extension is out of date
Sebastian Ullrich (Jul 22 2022 at 08:33):
Mario Carneiro said:
The Coq word for
sorryisadmitand the Isabelle version isoops
nitpick: The Isabelle version of sorry is sorry. oops aborts the current proof without registering its declaration.
Sebastian Ullrich (Jul 22 2022 at 08:34):
So I would not be surprised if Lean sorry is derived from Isabelle
Last updated: Dec 20 2023 at 11:08 UTC