Leonardo de Moura cc6104b369 fix: bug in the old frontend ... It had to be fixed because we have code that needs to be compiled with the old frontend, and the hacks we used to workaround this issue are incompatible with the new frontend.		2020-09-11 14:12:03 -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
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	chore: moving tests to new frontend	2020-09-10 18:00:34 -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: improve choice nodes + postpone	2020-09-11 12:45:38 -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
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	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
emptyc.lean	feat: elaborate emptyC notation	2020-09-11 10:42:39 -07: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	chore: fix tests	2020-05-26 15:05:00 -07:00
extern.lean
extmacro.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
finally.lean	feat: add MonadFinally	2020-08-25 17:58:35 -07:00
float1.lean	feat: expose some transcendental functions from the C library	2020-04-06 15:22:25 -07:00
float_cases_bug.lean
float_from_bignum.lean	feat: Float from big numbers	2020-04-06 14:05:17 -07:00
floatarray.lean	feat: add FloatArray	2020-04-07 18:05:54 -07:00
foldConsts.lean	chore: fix tests	2020-05-26 15:05:01 -07:00
frontend1.lean	feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
fun.lean
generalize.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
generalizeTelescope.lean	chore: fix tests	2020-08-24 17:59:11 -07:00
genindices.lean	chore: fix tests	2020-05-26 15:05:01 -07:00
getline_crash.lean	chore: fix test	2020-03-23 15:47:51 -07:00
handlers.lean
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
induction1.lean	feat: refine refine tactic	2020-08-30 16:14:38 -07:00
inductive1.lean	feat: new inductive command syntax	2020-09-02 09:41:52 -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: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
inline_fn.lean
inliner_loop.lean
instances.lean	fix: freeing Environments in tests	2020-07-10 07:42:26 -07:00
instuniv.lean	fix: freeing Environments in tests	2020-07-10 07:42:26 -07:00
int_to_nat_bug.lean
intromacro.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
IO_test.lean	chore: moving tests to new frontend	2020-09-10 18:00:34 -07:00
irCompilerBug.lean	test: add test for buggy compiler step	2020-08-26 08:34:35 -07:00
kernel1.lean	feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
kernel2.lean	feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
kevin.lean	feat: adjust semantics to new syntax	2020-08-19 09:56:23 -07:00
level.lean	chore: fix tests	2020-05-26 15:05:00 -07:00
LiftMethodIssue.lean	chore: fix test	2020-02-11 16:26:39 -08:00
listDecEq.lean	feat: add withPtrEqDecEq (version of withPtrEq for implementing decidable equality)	2020-02-15 16:12:09 -08: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
macro_macro.lean
macroid.lean	feat: adjust semantics to new syntax	2020-08-19 09:56:23 -07:00
match1.lean	test: add match with proofs example	2020-09-09 16:59:45 -07:00
matchArrayLit.lean	feat: add auxiliary definitions for compiling array literals in pattern matching expressions	2020-08-07 09:23:33 -07:00
matchtac.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
meta1.lean	chore: fix tests	2020-08-24 12:17:47 -07:00
meta2.lean	chore: fix tests	2020-08-24 17:59:11 -07:00
meta3.lean	chore: fix tests	2020-08-23 19:58:41 -07:00
meta4.lean	chore: fix some tests	2020-08-20 18:36:29 -07:00
meta5.lean	chore: fix tests	2020-08-24 17:59:11 -07:00
meta6.lean	chore: remove workaround	2020-08-26 16:24:20 -07:00
meta7.lean	fix: avoid unnecessary reduction	2020-09-06 06:57:52 -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	feat: add Expr.forEach	2020-09-08 13:03:53 -07:00
monadControl.lean	test: MonadControl	2020-08-25 13:54:41 -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
new_compiler.lean	chore: fix tests	2020-05-12 15:02:03 -07:00
new_frontend2.lean	fix: too restrictive condition	2020-09-10 11:20:09 -07:00
new_inductive.lean	chore: fix tests	2020-05-12 15:02:03 -07:00
new_inductive2.lean
newfrontend1.lean	feat: refine refine tactic	2020-08-30 16:14:38 -07:00
newfrontend2.lean
newfrontend3.lean	feat: abstract proofs occurring in binders	2020-09-08 12:29:35 -07:00
newfrontend4.lean	doc: document why example fails	2020-02-12 13:46:55 -08:00
newfrontend5.lean	refactor: remove support for fun {a : A} => ...	2020-03-26 10:40:16 -07:00
noncomputable_bug.lean
obtain.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
parseCore.lean	chore: fix tests	2020-05-26 15:05:00 -07:00
partial1.lean	fix: mkLetRecClosureFor	2020-09-08 15:14:46 -07:00
patbug.lean	fix: to_pattern_fn bug	2020-03-17 12:58:08 -07:00
print_cmd.lean	feat: elaborate #print command	2020-07-28 16:24:16 -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: fix test	2020-02-15 16:15:37 -08:00
quasi_pattern_unification_approx_issue.lean
rc_tests.lean
readerThe.lean	feat: add adaptTheReader	2020-08-19 10:23:11 -07:00
recInfo1.lean	chore: fix tests	2020-05-26 15:05:00 -07:00
reduce1.lean	feat: allow decide! and nativeDecide! take _ as an argument	2020-03-18 16:00:06 -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: fix tests	2020-05-26 15:05:01 -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	feat: add Tarjan's SCC	2020-09-06 14:19:59 -07:00
sharecommon.lean	chore: fix tests	2020-06-25 11:58:49 -07:00
stateRef.lean	feat: real ST monad	2020-08-23 12:15:32 -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: test for simulating old { Prod . ... } syntax	2020-05-20 16:06:57 -07:00
struct_instance_in_eqn.lean	chore: { <source> with ... } syntax	2020-05-20 15:08:43 -07:00
structInst.lean	chore: fix some tests	2020-05-21 09:50:20 -07:00
structInst2.lean	chore: fix tests	2020-05-12 15:02:03 -07:00
structInst3.lean	chore: fix some tests	2020-05-21 09:50:20 -07:00
structInst4.lean	chore: fix some tests	2020-05-21 09:50:20 -07:00
structure.lean	feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
subst1.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
synth1.lean	chore: fix tests	2020-05-26 15:05:00 -07:00
synthPending1.lean	feat: synthPending implementation	2020-03-13 13:52:00 -07:00
tactic.lean	chore: fix tests	2020-05-26 15:05:00 -07:00
tactic1.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
tacticExtOverlap.lean	chore: "begin ... end" ==> "by { ... }"	2020-08-30 14:01:27 -07:00
task_test.lean
task_test2.lean
termElab.lean	chore: fix tests	2020-08-24 17:59:11 -07:00
termParserAttr.lean	feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
termparsertest1.lean	chore: fix tests	2020-05-26 15:05:00 -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: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions	2020-08-22 16:00:43 -07:00
trace.lean	refactor: simplify Util/Trace.lean	2020-08-28 17:36:44 -07:00
tryPureCoe.lean	feat: add tryPureCoe	2020-03-27 11:20:43 -07:00
type_class_performance1.lean
typeclass_append.lean	chore: reduce stack space requirements in test	2020-08-13 12:13:38 -07:00
typeclass_coerce.lean
typeclass_diamond.lean	fix: do not consider auxiliary declarations as local instances	2020-09-07 08:08:35 -07:00
typeclass_easy.lean
typeclass_loop.lean	test: example that requires the instance arg reordering	2020-04-08 16:56:14 -07:00
typeclass_metas_internal_goals1.lean
typeclass_metas_internal_goals2.lean
typeclass_metas_internal_goals3.lean
typeclass_metas_internal_goals4.lean
typeclass_outparam.lean
ubscalar.lean	chore: { <source> with ... } syntax	2020-05-20 15:08:43 -07:00
unexpected_result_with_bind.lean	fix: typo at IR.Expr.alphaEqv	2020-03-31 10:04:59 -07:00
unif_issue.lean	chore: fix tests	2020-05-26 15:05:01 -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