max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean
History
Leonardo de Moura b2bc2d2775 feat: improve field notation argument search 
@Kha the new test may look exoteric, but it reflects an actual
instance in our code base, and the old frontend supports it.
Not sure whether we should keep it or not.
2020-10-16 14:32:03 -07:00
..
newfrontend
run feat: improve field notation argument search 2020-10-16 14:32:03 -07:00
server chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
trust0
.gitignore chore: ignore test output files 2020-08-31 11:09:27 +02:00
abst.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
abst.lean.expected.out
appParserIssue.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
appParserIssue.lean.expected.out feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
attrCmd.lean feat: attribute command 2020-09-20 09:11:36 -07:00
attrCmd.lean.expected.out feat: attribute command 2020-09-20 09:11:36 -07:00
auxDeclIssue.lean feat: add option pp.macroStack 2020-09-16 15:29:28 -07:00
auxDeclIssue.lean.expected.out feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
binsearch.lean fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
binsearch.lean.expected.out
bytearray.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
bytearray.lean.expected.out feat: ByteArray.copySlice 2020-08-28 10:04:32 -07:00
class_def_must_fail.lean
class_def_must_fail.lean.expected.out
classBadOutParam.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
classBadOutParam.lean.expected.out chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
collectDepsIssue.lean fix: collectDeps issue 2020-09-13 09:47:00 -07:00
collectDepsIssue.lean.expected.out feat: hide auxiliary declarations 2020-09-15 16:50:16 -07:00
ctor_layout.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
ctor_layout.lean.expected.out feat: unsafe functions for freeing compacted regions 2020-07-10 07:42:26 -07:00
dbgMacros.lean feat: improve dbgTrace! macro 2020-10-13 12:38:04 -07:00
dbgMacros.lean.expected.out chore: fix tests 2020-10-05 11:28:52 -07:00
doNotation1.lean fix: error message location 2020-10-07 17:43:23 -07:00
doNotation1.lean.expected.out fix: error message location 2020-10-07 17:43:23 -07:00
doSeqRightIssue.lean test: do issue 2020-08-15 16:07:01 -07:00
doSeqRightIssue.lean.expected.out fix: remove duplicate error messages due to variable(s) 2020-09-14 12:44:25 -07:00
emptyc.lean feat: remove emptyc elaboration hack 2020-09-11 14:41:44 -07:00
emptyc.lean.expected.out feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
envExtensionSealed.lean chore: avoid memory leak 2020-09-21 13:30:58 -07:00
envExtensionSealed.lean.expected.out chore: remove old pretty printer 2020-10-15 12:04:55 +02:00
eval_except.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
eval_except.lean.expected.out
evalWithMVar.lean fix: lval resolution 2020-09-12 07:45:36 -07:00
evalWithMVar.lean.expected.out feat: improve error messages for unassigned metavariables 2020-09-29 17:18:03 -07:00
exitAfterParseError.lean fix: skip minimum amount of tokens during parser recovery 2020-09-21 11:37:50 +02:00
exitAfterParseError.lean.expected.out fix: skip minimum amount of tokens during parser recovery 2020-09-21 11:37:50 +02:00
extract.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
extract.lean.expected.out
file_not_found.lean refactor: elabAppArgsAux 2020-10-11 15:08:12 -07:00
file_not_found.lean.expected.out feat: indented do blocks 2020-09-14 13:44:51 -07:00
Format.lean fix: break grouped fill items containing hard line breaks 2020-10-14 14:24:47 +02:00
Format.lean.expected.out feat: Format.fill 2020-10-07 15:30:36 +02:00
holeErrors.lean feat: improve error messages for unassigned metavariables 2020-09-29 17:18:03 -07:00
holeErrors.lean.expected.out feat: improve error messages for unassigned metavariables 2020-09-29 17:18:03 -07:00
holes.lean test: add another missing hole test 2020-09-07 17:18:20 -07:00
holes.lean.expected.out refactor: elabAppArgsAux 2020-10-11 15:08:12 -07:00
hygienicIntro.lean feat: add hygienicIntro option 2020-09-18 13:02:38 -07:00
hygienicIntro.lean.expected.out feat: add hygienicIntro option 2020-09-18 13:02:38 -07:00
inductive1.lean feat: new inductive command syntax 2020-09-02 09:41:52 -07:00
inductive1.lean.expected.out chore: move to new frontend 2020-10-16 09:16:33 -07:00
infoFromFailure.lean fix: preserve info messages from candidates that failed to be elaborated 2020-09-17 17:08:14 -07:00
infoFromFailure.lean.expected.out refactor: simpler mechanism for never backtracking traces 2020-09-18 10:31:42 -07:00
inst.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
inst.lean.expected.out
IRbug.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
IRbug.lean.expected.out
json.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
json.lean.expected.out
letrec1.lean feat: validate 'let rec' types 2020-09-02 17:02:40 -07:00
letrec1.lean.expected.out feat: add option pp.macroStack 2020-09-16 15:29:28 -07:00
ll_infer_type_bug.lean refactor: elabAppArgsAux 2020-10-11 15:08:12 -07:00
ll_infer_type_bug.lean.expected.out fix: break grouped fill items containing hard line breaks 2020-10-14 14:24:47 +02:00
lvl1.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
lvl1.lean.expected.out
macroscopes.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
macroscopes.lean.expected.out
macroStack.lean fix: throwAppTypeMismatch should be polymorphic 2020-09-22 09:35:59 -07:00
macroStack.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
match1.lean fix: scope and improve error message 2020-09-09 16:44:43 -07:00
match1.lean.expected.out feat: add hygienicIntro option 2020-09-18 13:02:38 -07:00
match2.lean fix: instantiate metavariables in alternative local decls 2020-08-15 08:18:00 -07:00
match2.lean.expected.out fix: instantiate metavariables in alternative local decls 2020-08-15 08:18:00 -07:00
match3.lean chore: remove begin ... end syntax 2020-08-30 14:15:33 -07:00
match3.lean.expected.out fix: nontermination at DepElim 2020-08-16 11:07:44 -07:00
match4.lean fix: anonymous constructor elaborator 2020-08-17 17:32:11 -07:00
match4.lean.expected.out feat: structure instances with .. in patterns 2020-08-17 16:23:49 -07:00
matchErrorLocation.lean feat: add elabTermEnsuringType 2020-08-15 13:49:10 -07:00
matchErrorLocation.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
mutualdef1.lean chore: parameters do not need to match in mutually recursive definitions 2020-09-02 10:30:35 -07:00
mutualdef1.lean.expected.out chore: parameters do not need to match in mutually recursive definitions 2020-09-02 10:30:35 -07:00
mutualWithNamespaceMacro.lean feat: new inductive command syntax 2020-09-02 09:41:52 -07:00
mutualWithNamespaceMacro.lean.expected.out feat: mutual + namespace macro 2020-09-01 12:25:29 -07:00
mvar1.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
mvar1.lean.expected.out
mvar2.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
mvar2.lean.expected.out
mvar3.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
mvar3.lean.expected.out test: strip mvar suffixes 2020-09-15 09:32:00 -07:00
mvar_fvar.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
mvar_fvar.lean.expected.out
namedHoles.lean fix: multiple occurrences of named holes 2020-09-16 10:27:30 -07:00
namedHoles.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
namelit.lean
namelit.lean.expected.out
openExport.lean test: open and export 2020-09-15 10:46:40 -07:00
openExport.lean.expected.out feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
parserPrio.lean feat: add support for parser priorities in the syntax command 2020-09-19 18:47:08 -07:00
parserPrio.lean.expected.out feat: add support for parser priorities in the syntax command 2020-09-19 18:47:08 -07:00
phashmap_inst_coherence.lean chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
phashmap_inst_coherence.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
ppExpr.lean feat: delaborator: use nicer binder name for [anonymous] 2020-10-14 18:38:59 +02:00
ppExpr.lean.expected.out feat: delaborator: use nicer binder name for [anonymous] 2020-10-14 18:38:59 +02:00
PPRoundtrip.lean chore: cleanup 2020-09-28 19:05:48 -07:00
PPRoundtrip.lean.expected.out fix: Format.be: respect indent when trying to fit fill item in a new line 2020-10-14 14:24:47 +02:00
precissues.lean feat: change default precedence for new syntax 2020-09-21 19:04:03 -07:00
precissues.lean.expected.out fix: break grouped fill items containing hard line breaks 2020-10-14 14:24:47 +02:00
private.lean
private.lean.expected.out feat: activate new pretty printer 2020-09-17 08:12:28 -07:00
Process.lean fix: IO.Process.output 2020-09-29 08:01:10 -07:00
Process.lean.expected.out fix: IO.Process.output 2020-09-29 08:01:10 -07:00
protected.lean fix: protected 2020-09-14 13:09:04 -07:00
protected.lean.expected.out chore: fix tests 2020-10-05 11:28:52 -07:00
readlinkf.sh
ref1.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
ref1.lean.expected.out
Reformat.lean test: Reformat.lean: make output test 2020-10-14 14:24:47 +02:00
Reformat.lean.expected.out fix: break grouped fill items containing hard line breaks 2020-10-14 14:24:47 +02:00
repr_issue.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
repr_issue.lean.expected.out
resolveGlobalName.lean feat: add MonadResolveName type class 2020-10-10 11:33:52 -07:00
resolveGlobalName.lean.expected.out feat: add resolveGlobalConst and resolveGlobalConstNoOverload 2020-09-20 08:54:24 -07:00
rewrite.lean feat: rewrite tactic 2020-09-18 16:13:14 -07:00
rewrite.lean.expected.out feat: rewrite tactic 2020-09-18 16:13:14 -07:00
sanitizeMacroScopes.lean feat: sanitize Syntax in messages 2020-09-29 07:59:22 -07:00
sanitizeMacroScopes.lean.expected.out chore: move to new frontend 2020-10-16 11:57:19 -07:00
shadow.lean chore: improve sanitizeNames superscripts 2020-09-17 08:57:54 -07:00
shadow.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
stdio.lean refactor: elabAppArgsAux 2020-10-11 15:08:12 -07:00
stdio.lean.expected.out feat: make std streams Streams 2020-08-28 10:04:32 -07:00
string_imp.lean chore: move more tests to new frontend 2020-09-13 16:13:20 -07:00
string_imp.lean.expected.out
string_imp2.lean chore: move more tests to new frontend 2020-09-13 16:13:20 -07:00
string_imp2.lean.expected.out fix: String: take/drop characters, not bytes 2020-08-11 18:24:47 -07:00
struct1.lean chore: move more tests to new frontend 2020-09-13 16:13:20 -07:00
struct1.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
StxQuot.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
StxQuot.lean.expected.out test: remove broken test case 2020-09-17 08:12:28 -07:00
test_single.sh test: strip mvar suffixes 2020-09-15 09:32:00 -07:00
typeMismatch.lean fix: horrible error message due to constApprox := true 2020-09-29 07:54:48 -07:00
typeMismatch.lean.expected.out chore: fix error messages 2020-10-06 10:52:04 -07:00
typeOf.lean chore: improve error message 2020-10-06 10:45:12 -07:00
typeOf.lean.expected.out chore: suppress extraMsg in type mismatch errors 2020-10-06 10:58:50 -07:00
unused_univ.lean feat: report unused universe parameters 2020-07-14 16:40:56 -07:00
unused_univ.lean.expected.out feat: report unused universe parameters 2020-07-14 16:40:56 -07:00
zipper.lean fix: set constApprox := false at SynthInstance 2020-09-13 16:11:27 -07:00
zipper.lean.expected.out