max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/run
History
Leonardo de Moura 544d2f4ce5 fix: kind for type metavariable 
For example, `mkFreshExprMVar none MetavarKind.synthetic` should
create a fresh synthetic metavariable `?m` with type `?t` where `?t`
is a fresh natural metavariable. If users want a synthetic
metavariable `?t`, then it must create it themselves.
2020-09-16 08:24:15 -07:00
..
.gitignore chore: ignore more test output files 2020-05-14 14:38:52 +02:00
28.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
34.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
108.lean fix: closes #108 2020-02-01 23:17:00 -08:00
111.lean chore: fix tests 2020-05-26 15:05:01 -07:00
121.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
125.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
1954.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
1968.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
anonymous_ctor_error_msg.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
array1.lean fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
autoparam.lean feat: elaborate autoParams 2020-02-13 16:24:50 -08:00
backtrackable_estate.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
bigmul.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
bigop.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
borrowBug.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
catchThe.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
check.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
choiceExpectedTypeBug.lean feat: remove emptyc elaboration hack 2020-09-11 14:41:44 -07:00
choiceMacroRules.lean chore: fix test 2020-06-08 16:13:52 -07:00
closure1.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coeIssue1.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coeIssue2.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coeIssue3.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coeIssues4.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coelambda.lean fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
CoeNew.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
coeSort1.lean feat: simplify CoeFun and CoeSort 2020-01-29 21:56:26 -08:00
coeSort2.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
CommandExtOverlap.lean feat: delaborator: do not set whitespace information 2020-05-20 11:54:53 -07:00
compiler_proj_bug.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
constantCompilerBug.lean chore: fix tests 2020-05-26 15:05:01 -07:00
core.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
csimp_type_error.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
DefEqAssignBug.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
depElim1.lean chore: use new frontend 2020-09-10 19:34:05 -07:00
deriv.lean chore: move test to new frontend 2020-09-11 07:47:19 -07:00
dofun_prec.lean feat: change precedence for fun and do parsing rules to maxPrec 2020-06-11 16:24:04 -07:00
doNotation1.lean fix: do not lift (<- action) nested in quotations 2020-09-11 08:06:20 -07:00
elab_cmd.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
elabCmd.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
elabIte.lean feat: change ite and dite argument order 2020-02-03 14:11:29 -08:00
emptycOverloadIssues.lean fix: bug in the old frontend 2020-09-11 14:12:03 -07:00
etaFirst.lean test: unifier 2020-03-05 18:44:33 -08:00
eval_unboxed_const.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
evalconst.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
expectedTypePropagation.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
expr1.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
expr_maps.lean feat: remove emptyc elaboration hack 2020-09-11 14:41:44 -07:00
extern.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
extmacro.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
finally.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
float1.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
float_cases_bug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
float_from_bignum.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
floatarray.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
foldConsts.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
frontend1.lean refactor: move ppExpr to IO 2020-09-15 18:48:21 -07:00
fun.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
generalize.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
generalizeTelescope.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
genindices.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
getline_crash.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
implicitTypesRecCoe.lean feat: break PreDefinitions into strongly connected components 2020-09-06 14:22:06 -07:00
incmd.lean feat: expand in command macro 2020-09-02 10:04:58 -07:00
ind_cmd_bug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
induction1.lean feat: finish commit "using indentation" 2020-09-14 16:40:52 -07:00
inductive1.lean fix: check inductive datatype parameters in constructor resulting type 2020-09-14 16:56:13 -07:00
inductive2.lean feat: allow commands such as variable and universe in the preamble of a mutual command block 2020-07-16 09:55:51 -07:00
inj1.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
inj2.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
inline_fn.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
inliner_loop.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
instances.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
instuniv.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
int_to_nat_bug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
intromacro.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
IO_test.lean feat: indented do blocks 2020-09-14 13:44:51 -07:00
irCompilerBug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
kernel1.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
kernel2.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
kevin.lean feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
level.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
LiftMethodIssue.lean chore: fix test 2020-02-11 16:26:39 -08:00
listDecEq.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
macro.lean chore: fix some tests 2020-06-08 16:12:06 -07:00
macro2.lean fix: notation command 2020-06-09 14:11:34 -07:00
macro3.lean feat: add Array.getSepElems 2020-01-18 19:12:44 -08:00
macro_macro.lean fix: add workaround for setting correct LBP for $ in antiquotations 2020-01-20 10:42:58 -08:00
macroid.lean feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
match1.lean fix: expandMatchDiscr cannot be a macro 2020-09-15 13:29:28 -07:00
matchArrayLit.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
matchtac.lean fix: expandMatchDiscr cannot be a macro 2020-09-15 13:29:28 -07:00
meta1.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
meta2.lean feat: indented do blocks 2020-09-14 13:44:51 -07:00
meta3.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
meta4.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
meta5.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
meta6.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
meta7.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
mixedMacroRules.lean chore: fix tests 2020-06-08 16:18:46 -07:00
mixfix.lean feat: expand macros infix, infixl, infixr, prefix, and postfix 2020-09-07 16:35:25 -07:00
monadCache.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
monadControl.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
nativeReflBackdoor.lean feat: elaborate #print axioms command 2020-08-28 13:08:42 -07:00
natlit.lean fix: nat lit support 2020-03-13 06:54:33 -07:00
nested_match_bug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
new_compiler.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
new_frontend2.lean feat: finish commit "using indentation" 2020-09-14 16:40:52 -07:00
new_inductive.lean fix: bug at inductive datatype resulting universe inference 2020-09-11 16:07:22 -07:00
new_inductive2.lean chore: move more tests to new frontend 2020-09-11 16:28:57 -07:00
newfrontend1.lean chore: fix tests 2020-09-15 11:11:05 -07:00
newfrontend2.lean chore: move more tests to new frontend 2020-09-11 16:28:57 -07:00
newfrontend3.lean chore: move more tests to new frontend 2020-09-11 16:28:57 -07:00
newfrontend4.lean doc: document why example fails 2020-02-12 13:46:55 -08:00
newfrontend5.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
nicerNestedDos.lean feat: indented do blocks 2020-09-14 13:44:51 -07:00
noncomputable_bug.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
obtain.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
overloaded.lean fix: always ensure expectedType when processing overloaded symbols and/or notation 2020-09-13 11:59:13 -07:00
parseCore.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
partial1.lean fix: mkLetRecClosureFor 2020-09-08 15:14:46 -07:00
patbug.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
print_cmd.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
proofIrrelFVar.lean fix: isDefEqQuick 2020-08-15 13:24:43 -07:00
prv.lean fix: resolveGlobalName for atomic references to private names 2020-07-23 14:58:19 -07:00
ptrAddr.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
quasi_pattern_unification_approx_issue.lean fix: isDefEq configuration in the elaborator 2020-09-11 17:36:28 -07:00
rc_tests.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
readerThe.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
recInfo1.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
reduce1.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
reduce2.lean test: add rfl tests 2020-03-17 16:18:18 -07:00
reduce3.lean test: decide! tests 2020-03-18 16:48:28 -07:00
Reformat.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
Reid1.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
Reparen.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
replace.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
resolveLVal.lean feat: improve resolveLVal 2020-09-07 12:25:43 -07:00
revert1.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
scc.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
sharecommon.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
stateRef.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
struct1.lean test: basic tests for new structure command 2020-07-24 12:13:02 -07:00
struct2.lean fix: id marker for auxiliary _default declarations 2020-07-24 15:59:45 -07:00
struct3.lean test: structure 2020-07-27 16:07:19 -07:00
struct_inst_typed.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
struct_instance_in_eqn.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
structInst.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
structInst2.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
structInst3.lean fix: kind for type metavariable 2020-09-16 08:24:15 -07:00
structInst4.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
structure.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
subst1.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
synth1.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
synthPending1.lean feat: synthPending implementation 2020-03-13 13:52:00 -07:00
tactic.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
tactic1.lean test: have-by in tactic mode 2020-09-14 15:17:25 -07:00
tacticExtOverlap.lean chore: "begin ... end" ==> "by { ... }" 2020-08-30 14:01:27 -07:00
task_test.lean fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
task_test2.lean fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
task_test_io.lean feat: more IO Task functions 2020-09-14 17:57:33 +02:00
termElab.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
termParserAttr.lean refactor: move ppExpr to IO 2020-09-15 18:48:21 -07:00
termparsertest1.lean chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
test_single.sh chore: factor out and unify common test behavior; retrieve lean from PATH 2020-05-14 14:38:52 +02:00
toExpr.lean feat: extend/cleanup isLevelDefEqAux 2020-09-12 15:38:48 -07:00
trace.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
tryPureCoe.lean feat: add tryPureCoe 2020-03-27 11:20:43 -07:00
type_class_performance1.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_append.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_coerce.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_diamond.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_easy.lean feat: add #synth command to new frontend 2020-01-09 09:54:45 -08:00
typeclass_loop.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_metas_internal_goals1.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_metas_internal_goals2.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_metas_internal_goals3.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_metas_internal_goals4.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
typeclass_outparam.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
ubscalar.lean chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
unexpected_result_with_bind.lean fix: try to synthesize instance for substructures 2020-09-12 08:58:13 -07:00
unif_issue.lean feat: indented do blocks 2020-09-14 13:44:51 -07:00
unif_issue2.lean chore: fix tests 2020-05-26 15:05:01 -07:00
update.lean chore: fix tests 2020-05-26 15:05:00 -07:00
WindowsNewlines.lean fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00