Kyle Miller f336525f31 fix: make delabConstWithSignature avoid using inaccessible names (#3625) ... The `delabConstWithSignature` delaborator is responsible for pretty printing constants with a declaration-like signature, with binders, a colon, and a type. This is used by the `#check` command when it is given just an identifier. It used to accumulate binders from pi types indiscriminately, but this led to unfriendly behavior. For example, `#check String.append` would give ``` String.append (a✝ : String) (a✝¹ : String) : String ``` with inaccessible names. These appear because `String.append` is defined using patterns, so it never names these parameters. Now the delaborator stops accumulating binders once it reaches an inaccessible name, and for example `#check String.append` now gives ``` String.append : String → String → String ``` We do not synthesize names for the sake of enabling binder syntax because the binder names are part of the API of a function — one can use `(arg := ...)` syntax to pass arguments by name. The delaborator also now stops accumulating binders once it reaches a parameter with a name already seen before — we then rely on the main delaborator to provide that parameter with a fresh name when pretty printing the pi type. As a special case, instance parameters with inaccessible names are included as binders, pretty printing like `[LT α]`, rather than relegating them (and all the remaining parameters) to after the colon. It would be more accurate to pretty print this as `[inst✝ : LT α]`, but we make the simplifying assumption that such instance parameters are generally used via typeclass inference. Likely `inst✝` would not directly appear in pretty printer output, and even if it appears in a hover, users can likely figure out what is going on. (We may consider making such `inst✝` variables pretty print as `‹LT α›` or `infer_instance` in the future, to make this more consistent.) Something we note here is that we do not do anything to make sure parameters that can be used as named arguments actually appear named after the colon (nor do we assure that the names are the correct names). For example, one sees `foo : String → String → String` rather than `foo : String → (baz : String) → String`. We can investigate this later if it is wanted. We also give `delabConstWithSignature` a `universes` flag to enable turning off pretty printing universe levels parameters. Closes #2846		2024-03-07 18:14:06 +00:00
..
533.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
533.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
863.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
863.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
1031.lean
1031.lean.expected.out
1265.lean
1265.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
1403.lean
1403.lean.expected.out	feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences (#2539)	2024-01-03 00:01:40 +00:00
1525.lean	fix: missing info tree on elab failure	2023-01-26 13:05:57 +01:00
1525.lean.expected.out	fix: missing info tree on elab failure	2023-01-26 13:05:57 +01:00
1659.lean	feat: auto-complete declaration names in arbitrary namespaces	2023-07-28 07:50:09 -07:00
1659.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
amb.lean
amb.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
anonHyp.lean
anonHyp.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
autoBoundIssue.lean
autoBoundIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
catHover.lean
catHover.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
codeaction.lean	fix: version numbers in code actions (#2721)	2023-10-24 22:55:47 +11:00
codeaction.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
compHeader.lean
compHeader.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion.lean
completion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion2.lean
completion2.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion3.lean
completion3.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion4.lean
completion4.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion5.lean
completion5.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion6.lean
completion6.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion7.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
completion7.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionAtPrint.lean
completionAtPrint.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionCheck.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionCheck.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionDocString.lean
completionDocString.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionEOF.lean
completionEOF.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionFromExpectedType.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionFromExpectedType.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionIStr.lean
completionIStr.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOpenNamespaces.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOpenNamespaces.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOption.lean	chore: register pretty printer trace classes	2022-10-19 14:51:07 +02:00
completionOption.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrefixIssue.lean
completionPrefixIssue.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrivateTypes.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrivateTypes.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrv.lean
completionPrv.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
compNamespace.lean
compNamespace.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
definition.lean
definition.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
Diff.lean
Diff.lean.expected.out	refactor: diffTag → diffStatus	2022-10-06 13:06:31 -07:00
discrsIssue.lean
discrsIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
dotIdCompletion.lean
dotIdCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
editAfterError.lean
editAfterError.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
editCompletion.lean
editCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
fieldCompletion.lean
fieldCompletion.lean.expected.out	chore: set literal notation (#3348)	2024-02-19 23:22:36 +00:00
foldingRange.lean
foldingRange.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goalEOF.lean
goalEOF.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goalIssue.lean
goalIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goTo.lean	feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767)	2023-01-19 09:10:01 +00:00
goTo.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goTo2.lean	feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767)	2023-01-19 09:10:01 +00:00
goTo2.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
haveInfo.lean
haveInfo.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
highlight.lean
highlight.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hover.lean	feat: improve termination_by error messages (#3255)	2024-02-05 13:13:53 +00:00
hover.lean.expected.out	fix: make delabConstWithSignature avoid using inaccessible names (#3625)	2024-03-07 18:14:06 +00:00
hoverAt.lean
hoverAt.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverBinderUndescore.lean
hoverBinderUndescore.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverDot.lean
hoverDot.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverException.lean
hoverException.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
infoIssues.lean
infoIssues.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
internalNamesIssue.lean
internalNamesIssue.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
inWordCompletion.lean	feat: BitVec.ofNatLt and updates to use it (#3430)	2024-02-21 18:02:56 +00:00
inWordCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
jumpMutual.lean
jumpMutual.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
keywordCompletion.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
keywordCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
lean3HoverIssue.lean
lean3HoverIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
macroGoalIssue.lean
macroGoalIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
match.lean
match.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
matchPatternHover.lean
matchPatternHover.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
matchStxCompletion.lean
matchStxCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
partialNamespace.lean
partialNamespace.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
plainGoal.lean	fix: report goals in induction with parse error	2023-11-20 09:15:27 +01:00
plainGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
plainTermGoal.lean
plainTermGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
rename.lean	feat: rename request handler (#2462)	2023-11-21 13:10:52 +01:00
rename.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
run.lean	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00
stdOutput.lean
stdOutput.lean.expected.out
terminationBySuggestion.lean	feat: termination_by? (#3514)	2024-02-28 10:53:17 +00:00
terminationBySuggestion.lean.expected.out	feat: termination_by? (#3514)	2024-02-28 10:53:17 +00:00
test_single.sh
unterminatedDocComment.lean
unterminatedDocComment.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
userWidget.lean	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00
userWidget.lean.expected.out	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00