max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive
History
Sebastian Ullrich 4a4b4c1ef4 fix: mkAtomFrom: generate synthetic position like other *From functions 
Also consistently use binders as reference position for an elided binder type.
Before, type errors were always given extent 1, the length of the
synthetic `_` token.
2021-07-19 13:24:59 -07:00
..
533.lean fix: fixes #533 2021-06-29 15:20:46 -07:00
533.lean.expected.out fix: fixes #533 2021-06-29 15:20:46 -07:00
amb.lean fix: Info nodes for overloaded notation/declarations 2021-05-04 22:07:21 -07:00
amb.lean.expected.out fix: Info nodes for overloaded notation/declarations 2021-05-04 22:07:21 -07:00
completion.lean chore: simplify tests 2021-04-05 22:01:56 +02:00
completion.lean.expected.out fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
completion2.lean test: completion 2021-04-05 12:01:58 -07:00
completion2.lean.expected.out fix: propagate expected type 2021-04-05 20:00:05 -07:00
completion3.lean feat: elaborate auxiliary completion node 2021-04-05 19:07:39 -07:00
completion3.lean.expected.out fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
completion4.lean test: auto completion 2021-04-05 20:45:04 -07:00
completion4.lean.expected.out fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
completion5.lean chore: add completion test for the group issue 2021-04-07 22:46:08 -07:00
completion5.lean.expected.out fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
completion6.lean feat: include parent structures and aliases in dot notation auto completion 2021-04-08 19:22:31 -07:00
completion6.lean.expected.out feat: include parent structures and aliases in dot notation auto completion 2021-04-08 19:22:31 -07:00
completion7.lean test: completion 2021-04-12 22:32:27 -07:00
completion7.lean.expected.out test: completion 2021-04-12 22:32:27 -07:00
completionEOF.lean fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
completionEOF.lean.expected.out fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
completionIStr.lean feat: improved error recovery for interpolated strings 2021-04-24 10:24:57 -07:00
completionIStr.lean.expected.out feat: improved error recovery for interpolated strings 2021-04-24 10:24:57 -07:00
completionOption.lean chore: auto-insert newlines 2021-07-05 19:42:01 +02:00
completionOption.lean.expected.out chore: auto-insert newlines 2021-07-05 19:42:01 +02:00
completionPrv.lean fix: fixes #408 2021-04-22 19:07:03 -07:00
completionPrv.lean.expected.out fix: fixes #408 2021-04-22 19:07:03 -07:00
definition.lean fix: server: go to type definition 2021-04-08 18:54:53 +02:00
definition.lean.expected.out fix: server: go to type definition 2021-04-08 18:54:53 +02:00
editAfterError.lean fix: server: do not stop processing after error (except for header error) 2021-04-12 22:41:10 +02:00
editAfterError.lean.expected.out feat: send $/lean/fileProgress notification 2021-06-05 13:49:28 +02:00
editCompletion.lean fix: watchdog: do not reorder messages while delaying edits 2021-04-07 17:12:37 +02:00
editCompletion.lean.expected.out fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
goalEOF.lean fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
goalEOF.lean.expected.out fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
goalIssue.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
goalIssue.lean.expected.out fix: missing tactic state info on broken proofs 2021-04-18 20:13:02 -07:00
goTo.lean chore: remove absolute paths from test 2021-07-05 19:42:01 +02:00
goTo.lean.expected.out chore: remove absolute paths from test 2021-07-05 19:42:01 +02:00
haveInfo.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
haveInfo.lean.expected.out chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
hover.lean fix: mkAtomFrom: generate synthetic position like other *From functions 2021-07-19 13:24:59 -07:00
hover.lean.expected.out fix: mkAtomFrom: generate synthetic position like other *From functions 2021-07-19 13:24:59 -07:00
hoverDot.lean feat: add dot hover test 2021-07-19 09:55:37 +02:00
hoverDot.lean.expected.out fix: hovers on elabFieldName fields 2021-07-19 09:55:37 +02:00
hoverException.lean fix: swallow exception on hover formatting 2021-06-23 23:29:46 +02:00
hoverException.lean.expected.out fix: swallow exception on hover formatting 2021-06-23 23:29:46 +02:00
macroGoalIssue.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
macroGoalIssue.lean.expected.out test: for tactic state visualization bug 2021-05-17 15:12:50 -07:00
match.lean feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
match.lean.expected.out feat: improve error recovery at Tactic.elabTerm 2021-05-06 20:44:36 -07:00
matchStxCompletion.lean feat: better error recovery for match syntax 2021-05-02 17:00:35 -07:00
matchStxCompletion.lean.expected.out feat: better error recovery for match syntax 2021-05-02 17:00:35 -07:00
partialNamespace.lean fix: documentHighlight on partial input 2021-05-11 17:03:18 +02:00
partialNamespace.lean.expected.out fix: documentHighlight on partial input 2021-05-11 17:03:18 +02:00
plainGoal.lean fix: tactic state on {/· 2021-05-21 17:13:33 -07:00
plainGoal.lean.expected.out fix: tactic state on {/· 2021-05-21 17:13:33 -07:00
plainTermGoal.lean feat: plain term goal request 2021-06-07 16:23:22 -07:00
plainTermGoal.lean.expected.out fix: mkAtomFrom: generate synthetic position like other *From functions 2021-07-19 13:24:59 -07:00
run.lean fix: server: completion & goal state at EOF 2021-04-30 19:25:53 +02:00
stdOutput.lean fix: isolate std streams for all commands in server mode 2021-05-19 13:30:54 +02:00
stdOutput.lean.expected.out fix: isolate std streams for all commands in server mode 2021-05-19 13:30:54 +02:00
test_single.sh chore: disable LSAN in server tests for now 2021-06-23 08:53:20 +02:00