-
Notifications
You must be signed in to change notification settings - Fork 388
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
Should .below
be marked as private/internal?
#4701
Comments
Pinging @arthur-adjedj for an opinion? |
When having invalid pattern, constructor or constant marked with '[match_pattern]' expected
Suggestions:
'Batteries.AssocList.cons',
'Batteries.BinomialHeap.Imp.Heap.cons',
'Batteries.RBNode.Stream.cons',
'IO.AsyncList.cons',
'LazyList.cons',
'Lean.AssocList.cons',
'List.Chain.below.cons',
'List.Chain.cons',
'List.Forall₂.below.cons',
'List.Forall₂.cons',
(or 7 others) I don't think there are many cases in which proving a |
I agree that it should not be suggested like this. I wouldn't hide it completely, it's useful for learning and for advanced uses, but not a good suggestion. |
JFTR: I anticipate that at some point we’ll have to get more clarity on the different notions of internal/private/etc that we have floating around, and their relevance for documentation listing/loogle/tactics/error message suggestions. When that comes up hopefully it’ll be clearer what to do here. |
See for example
In
tests/lean/run/constructor_as_variable.lean
we now see the error:on the test
These
.below
auxiliary functions are rarely (never?) meant to be used by users, and perhaps should be marked as private or internal in some way, so they would not be displayed here.There is already a check for
isPrivateName
when generating this message.The text was updated successfully, but these errors were encountered: