This website requires JavaScript.
Explore
Help
Sign in
max
/
lean4-htt
Watch
1
Star
0
Fork
You've already forked lean4-htt
0
Code
Issues
Pull requests
Projects
Releases
Packages
Wiki
Activity
Actions
2
2a1aee2b7a
lean4-htt
/
tests
/
lean
/
interactive
History
larsk21
e641ae4eae
fix: prefix check in set_option completion
2021-11-26 11:42:54 +01:00
..
533.lean
533.lean.expected.out
amb.lean
amb.lean.expected.out
completion.lean
completion.lean.expected.out
completion2.lean
completion2.lean.expected.out
feat: avoid metavariables at
CompletionItem
s
2021-10-29 08:01:21 -07:00
completion3.lean
completion3.lean.expected.out
completion4.lean
completion4.lean.expected.out
completion5.lean
completion5.lean.expected.out
completion6.lean
completion6.lean.expected.out
completion7.lean
completion7.lean.expected.out
feat: avoid metavariables at
CompletionItem
s
2021-10-29 08:01:21 -07:00
completionDocString.lean
completionDocString.lean.expected.out
feat: avoid metavariables at
CompletionItem
s
2021-10-29 08:01:21 -07:00
completionEOF.lean
completionEOF.lean.expected.out
completionIStr.lean
completionIStr.lean.expected.out
completionOption.lean
fix: prefix check in set_option completion
2021-11-26 11:42:54 +01:00
completionOption.lean.expected.out
fix: prefix check in set_option completion
2021-11-26 11:42:54 +01:00
completionPrv.lean
completionPrv.lean.expected.out
definition.lean
definition.lean.expected.out
editAfterError.lean
editAfterError.lean.expected.out
editCompletion.lean
editCompletion.lean.expected.out
goalEOF.lean
goalEOF.lean.expected.out
goalIssue.lean
goalIssue.lean.expected.out
goTo.lean
fix: go to definition for
macro_rules
etc.
2021-11-24 11:54:13 +01:00
goTo.lean.expected.out
fix: go to definition for
macro_rules
etc.
2021-11-24 11:54:13 +01:00
haveInfo.lean
haveInfo.lean.expected.out
hover.lean
fix: handle _root_ in unresolveNameGlobal with pp.fullNames
2021-11-21 15:23:21 +01:00
hover.lean.expected.out
fix: handle _root_ in unresolveNameGlobal with pp.fullNames
2021-11-21 15:23:21 +01:00
hoverDot.lean
feat: show fully-qualified name in hover text
2021-11-21 15:23:21 +01:00
hoverDot.lean.expected.out
feat: show fully-qualified name in hover text
2021-11-21 15:23:21 +01:00
hoverException.lean
hoverException.lean.expected.out
macroGoalIssue.lean
macroGoalIssue.lean.expected.out
match.lean
match.lean.expected.out
matchStxCompletion.lean
matchStxCompletion.lean.expected.out
partialNamespace.lean
partialNamespace.lean.expected.out
plainGoal.lean
plainGoal.lean.expected.out
plainTermGoal.lean
plainTermGoal.lean.expected.out
run.lean
stdOutput.lean
stdOutput.lean.expected.out
test_single.sh
unterminatedDocComment.lean
unterminatedDocComment.lean.expected.out