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 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
..
.gitignore
28.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
29.lean test: issue 29 2020-09-23 18:30:28 -07:00
34.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
108.lean
111.lean
121.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
125.lean test: string interpolation 2020-10-09 17:02:12 -07:00
175.lean fix: fixes #175 2020-09-21 17:12:07 -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 test: new frontend tests 2020-10-09 18:21:45 -07:00
anonymousCtor.lean fix: anonymous constructor too restrictive 2020-10-16 07:58:47 -07:00
array1.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
autoparam.lean
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: remove Monad List instance 2020-10-05 13:27:18 -07:00
borrowBug.lean test: new frontend tests 2020-10-09 18:21:45 -07:00
catchThe.lean feat: add string interpolation for MessageData 2020-10-09 20:43:26 -07:00
cdotTests.lean test: cdot tests 2020-09-25 18:48:23 -07:00
check.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
choiceExpectedTypeBug.lean test: new frontend tests 2020-10-09 18:21:45 -07:00
choiceMacroRules.lean
closure1.lean feat: add string interpolation for MessageData 2020-10-09 20:43:26 -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 fix: tests and elabDo 2020-09-26 19:12:01 -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
coeSort2.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
CommandExtOverlap.lean test: new frontend 2020-09-29 18:22:34 -07:00
compiler_proj_bug.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
constantCompilerBug.lean
core.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
csimp_type_error.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
def1.lean fix: processNonVariable 2020-09-24 17:16:50 -07:00
def2.lean test: add old Lean3 tests 2020-09-24 17:32:47 -07:00
def3.lean test: add old Lean3 tests 2020-09-24 17:32:47 -07:00
def4.lean fix: bug at toBelow 2020-09-24 17:38:51 -07:00
def5.lean test: add old Lean3 tests 2020-09-24 18:01:23 -07:00
def6.lean test: add old Lean3 tests 2020-09-24 18:01:23 -07:00
def7.lean feat: optional ; in terms 2020-09-28 17:10:59 -07:00
def8.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def9.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def10.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def11.lean fix: missing case 2020-09-25 06:48:51 -07:00
def12.lean fix: visit types 2020-09-25 06:48:51 -07:00
def13.lean fix: visit types 2020-09-25 06:48:51 -07:00
def14.lean fix: visit types 2020-09-25 06:48:51 -07:00
def15.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def16.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def17.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def18.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def19.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
def20.lean test: add old Lean3 tests 2020-09-25 06:48:51 -07:00
DefEqAssignBug.lean test: new frontend 2020-09-29 18:22:34 -07:00
depElim1.lean feat: add string interpolation for MessageData 2020-10-09 20:43:26 -07:00
deriv.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
dofun_prec.lean test: new frontend tests 2020-10-09 18:21:45 -07:00
dollarProjIssue.lean fix: dollarProj notation bug 2020-10-10 13:38:07 -07:00
doNotation1.lean chore: move tests to new frontend 2020-10-10 07:41:04 -07:00
doNotation2.lean feat: improve dbgTrace! macro 2020-10-13 12:38:04 -07:00
doNotation3.lean feat: add doElem.quot elaboration function 2020-10-08 13:50:25 -07:00
doNotation4.lean test: string interpolation 2020-10-09 17:02:12 -07:00
doNotation5.lean feat: improve dbgTrace! macro 2020-10-13 12:38:04 -07:00
doNotation6.lean feat: array slicing notation 2020-10-09 16:40:18 -07:00
doTrailingAtEOI.lean fix: trailing ';' at end of input 2020-09-27 16:58:23 -07:00
eagerInliningIssue.lean perf: add temporary hack for performance issue 2020-10-15 13:37:29 -07:00
elab_cmd.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
elabCmd.lean chore: add temporary workaround to tests 2020-09-27 06:58:10 -07:00
elabIte.lean
emptycOverloadIssues.lean fix: bug in the old frontend 2020-09-11 14:12:03 -07:00
etaFirst.lean
eval_unboxed_const.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
evalconst.lean test: new frontend tests 2020-10-09 18:21:45 -07:00
expectedTypePropagation.lean chore: move more tests to new frontend 2020-09-11 10:28:00 -07:00
expr1.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
expr_maps.lean chore: add temporary workarounds 2020-09-30 07:05:46 -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
fieldIssue.lean feat: improve field notation argument search 2020-10-16 14:32:03 -07:00
finally.lean test: new frontend 2020-10-09 13:20:04 -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: add temporary workarounds 2020-09-30 07:05:46 -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
forBodyResultTypeIssue.lean feat: add Repr and HasToString instances for PUnit and ULift 2020-10-12 11:01:59 -07:00
frontend1.lean fix: horrible error message due to constApprox := true 2020-09-29 07:54:48 -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 test: new frontend 2020-10-09 13:20:04 -07:00
genindices.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
getline_crash.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
impByNameResolution.lean fix: use resolveGlobalConstNoOverload at implementedBy attribute handler 2020-10-10 11:40:32 -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 test: optional ';' 2020-09-28 17:11:00 -07:00
inductive1.lean fix: check inductive datatype parameters in constructor resulting type 2020-09-14 16:56:13 -07:00
inductive2.lean
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: add temporary workaround to tests 2020-09-27 06:58:10 -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 test: new frontend tests 2020-10-09 18:21:45 -07:00
irCompilerBug.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
kernel1.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
kernel2.lean fix: tests and elabDo 2020-09-26 19:12:01 -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 feat: remove old elabDo 2020-10-04 17:14:36 -07:00
listDecEq.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
localNameResolutionWithProj.lean fix: local name resolution 2020-10-05 17:32:46 -07:00
macro.lean
macro2.lean
macro3.lean
macro_macro.lean
macroid.lean feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
match1.lean fix: elabDiscrsWitMatchType 2020-10-15 11:00:33 -07:00
matchArrayLit.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
matchDiscrType.lean fix: (try to) postpone when discriminant type is not known 2020-10-10 16:16:22 -07:00
matcherElimUniv.lean fix: the generated matcher must be able to eliminate into different universe levels 2020-09-24 19:34:14 -07:00
matchNoPostponing.lean fix: synthesizeSyntheticMVarsNoPostponing at elabMatch 2020-10-15 10:44:16 -07:00
matchtac.lean fix: missing checkColGt and tests 2020-09-28 17:10:59 -07:00
meta1.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
meta2.lean test: new frontend 2020-09-29 18:22:34 -07:00
meta3.lean chore: add temporary workaround to tests 2020-09-27 06:58:10 -07:00
meta4.lean chore: cleanup 2020-09-28 19:05:48 -07:00
meta5.lean feat: add string interpolation for MessageData 2020-10-09 20:43:26 -07:00
meta6.lean chore: cleanup 2020-09-28 19:05:48 -07:00
meta7.lean chore: cleanup 2020-09-28 19:05:48 -07:00
mixedMacroRules.lean
mixfix.lean feat: expand macros infix, infixl, infixr, prefix, and postfix 2020-09-07 16:35:25 -07:00
monadCache.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
monadControl.lean chore: adjust test 2020-10-04 16:19:50 -07:00
namespaceIssue.lean fix: old&new frontend interference 2020-09-20 08:25:45 -07:00
nativeReflBackdoor.lean feat: elaborate #print axioms command 2020-08-28 13:08:42 -07:00
natlit.lean
nested_match_bug.lean chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
nestedDo.lean feat: expand nested dos 2020-10-15 17:11:50 -07:00
new_compiler.lean fix: horrible error message due to constApprox := true 2020-09-29 07:54:48 -07:00
new_frontend2.lean test: new frontend 2020-09-29 18:22:34 -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: remove workaround 2020-10-06 08:28:41 -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
newfrontend5.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
nicerNestedDos.lean test: new frontend 2020-09-29 18:22:34 -07:00
noncomputable_bug.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
obtain.lean test: new frontend 2020-09-29 18:22:34 -07:00
optParam.lean fix: handle optParam at consumeImplicits 2020-10-11 15:26:10 -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 fix: tests and elabDo 2020-09-26 19:12:01 -07:00
partial1.lean test: new frontend 2020-09-29 18:22:34 -07:00
partialApp.lean refactor: elabAppArgsAux 2020-10-11 15:08:12 -07:00
patbug.lean test: new frontend 2020-09-29 18:22:34 -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
ptrAddr.lean chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
quasi_pattern_unification_approx_issue.lean test: new frontend 2020-09-29 18:22:34 -07:00
range.lean feat: add Range notation 2020-10-12 11:50:13 -07:00
rc_tests.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
readerThe.lean feat: add withReader method 2020-10-13 15:00:17 -07:00
recInfo1.lean test: new frontend 2020-09-29 18:22:34 -07:00
reduce1.lean chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
reduce2.lean
reduce3.lean
Reid1.lean chore: moving tests to new frontend 2020-09-10 18:00:34 -07:00
Reparen.lean chore: add temporary workarounds 2020-09-30 07:05:46 -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 test: new frontend tests 2020-10-09 18:21:45 -07:00
sharecommon.lean test: new frontend tests 2020-10-09 18:21:45 -07:00
spec_issue.lean test: new frontend 2020-09-29 18:22:34 -07:00
stateRef.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
strInterpolation.lean feat: add interpolated string for toString 2020-10-09 14:38:24 -07:00
struct1.lean
struct2.lean
struct3.lean
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: add temporary workaround to tests 2020-09-27 06:58:10 -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
structuralIssue.lean feat: improve Structural.lean 2020-10-12 16:58:30 -07:00
structuralRec1.lean test: new tests for structural recursion 2020-09-23 18:24:56 -07:00
structure.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
stxKindInsideNamespace.lean fix: explicit syntax kind in macro_rules 2020-10-10 06:42:45 -07:00
stxMacro.lean test: new frontend 2020-10-09 13:20:04 -07:00
subst1.lean test: new frontend 2020-09-29 18:22:34 -07:00
synth1.lean test: new frontend 2020-09-29 18:22:34 -07:00
synthPending1.lean
tactic.lean test: new frontend 2020-09-29 18:22:34 -07:00
tactic1.lean fix: missing checkColGt and tests 2020-09-28 17:10:59 -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 feat: improve dbgTrace! macro 2020-10-13 12:38:04 -07:00
task_test_io.lean feat: more IO Task functions 2020-09-14 17:57:33 +02:00
termElab.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
termParserAttr.lean fix: horrible error message due to constApprox := true 2020-09-29 07:54:48 -07:00
termparsertest1.lean chore: add temporary workaround to tests 2020-09-27 06:58:10 -07:00
test_single.sh
toExpr.lean chore: add temporary workarounds 2020-09-30 07:05:46 -07:00
trace.lean feat: add withReader method 2020-10-13 15:00:17 -07:00
tryPureCoe.lean test: new frontend tests 2020-10-09 18:21:45 -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 fix: horrible error message due to constApprox := true 2020-09-29 07:54:48 -07:00
typeclass_diamond.lean feat: pretty print Syntax in messages 2020-09-29 07:59:22 -07:00
typeclass_easy.lean feat: pretty print Syntax in messages 2020-09-29 07:59:22 -07:00
typeclass_loop.lean fix: tests and elabDo 2020-09-26 19:12:01 -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: tests and elabDo 2020-09-26 19:12:01 -07:00
unif_issue.lean fix: tests and elabDo 2020-09-26 19:12:01 -07:00
unif_issue2.lean
update.lean
WindowsNewlines.lean