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 91dca53274 refactor: remove MonadIO 
There is no reason for having `MonadIO` anymore. The `MonadLift` type
class is well behaved in the new frontend, the `MonadFinally` solves
the problem at monad stacks such as `ExcepT e IO`.

This commit also changes the type of the IO printing functions.
For example, the type of `IO.println` was
```
def IO.println {m} [MonadIO m] {α} [ToString α] (s : α) : m Unit
```
and now it is just
```
def IO.println {α} [ToString α] (s : α) : IO Unit
```
We rely on the new frontend auto-lifting feature.
That is, if there is an instance `[MonadLiftT IO m]`, then
a term of type `IO a` is automatically coerced to `m a`

We also want a simpler `IO.println` for writing tests.
For example,
```
```
doesn't work because there isn't sufficient information for inferring
the parameter `m` in the previous `IO.println`.
The shortest workaround looked very weird
```
```

I considered adding `IO` as a default value for `m` when we have
`MonadIO m`, as we use `Nat` as the default for `ofNat a`, but it felt
like uncessary complexity.

@Kha The commit seems to work well. The auto-lifting featuring has
been working great for me. There is still room for improvement.
For example, given `MonadLiftT m n`, it doesn't automatically lift
`a -> m b` into `a -> n b`. So, code such as
`foo >>= IO.println`
had to be rewritten as
`foo >>= fun x => IO.println x`
I will add this feature later.
If you have time, please try to play with this feature and figure out
if it is stable enough for making it the default.
That is, if it roboust enough, we can stop using the following idiom
for writing functions that can be lifted automatically.
```
def instantiateLevelMVarsImp (u : Level) : MetaM Level :=
  ...

def instantiateLevelMVars {m} [MonadLiftT MetaM m] (u : Level) : m Level :=
  liftMetaM $ instantiateLevelMVarsImp u
```
I think we only need this idiom when using `MonadControlT` which is
not as common as `MonadLiftT`.
2020-11-18 18:47:22 -08:00
..
.gitignore chore: ignore more test output files 2020-05-14 14:38:52 +02:00
28.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
29.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
34.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
52_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
91_lean3.lean chore: remove misleading comment 2020-11-14 18:07:19 -08:00
102_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
108.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
111.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
121.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
125.lean chore: HasRepr ==> Repr 2020-10-27 16:15:10 -07:00
175.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
436_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
447_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
470_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
474_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
492_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
500_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
1954.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
1968.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
anonymous_ctor_error_msg.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
anonymousCtor.lean fix: anonymous constructor too restrictive 2020-10-16 07:58:47 -07:00
array1.lean chore: fix test 2020-11-17 17:14:06 -08:00
autoLiftIssue.lean feat: improve tryLiftAndCoe 2020-10-29 12:46:04 -07:00
autoparam.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
backtrackable_estate.lean chore: HasRepr ==> Repr 2020-10-27 16:15:10 -07:00
beginEndAsMacro.lean fix: stdlib and tests 2020-11-12 07:12:30 -08:00
bigmul.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
bigop.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
binderNotation.lean feat: improve mkLevelMax' 2020-11-14 08:36:23 -08:00
borrowBug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
casesUsing.lean feat: support for _ and ?hole at all induction/cases variants 2020-11-03 17:20:53 -08:00
catchThe.lean chore: add expandInterpolatedStr helper function, rename msg! => m! 2020-11-14 13:52:52 -08:00
cdotTests.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
check.lean chore: fix tests 2020-11-02 19:33:08 -08:00
checkAssignmentIssue.lean feat: improve local context reduction approximation 2020-10-31 19:19:18 -07:00
choiceExpectedTypeBug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
choiceMacroRules.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
closure1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeIssue1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeIssue2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeIssue3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeIssues4.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coelambda.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
CoeNew.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeSort1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
coeSort2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
CommandExtOverlap.lean fix: stdlib and tests 2020-11-12 07:12:30 -08:00
compiler_proj_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
concatElim.lean fix: beta reduce value at processAssignmentFOApprox 2020-11-12 14:46:28 -08:00
constantCompilerBug.lean chore: fix tests 2020-11-11 10:19:14 -08:00
core.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
csimp_type_error.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def4.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def5.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def6.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def7.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def8.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def9.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def10.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def11.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def12.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def13.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def14.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def15.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def16.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def17.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def18.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def19.lean chore: disable test until we implement "smart unfolding" 2020-11-03 17:20:53 -08:00
def20.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
DefEqAssignBug.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
depElim1.lean chore: add expandInterpolatedStr helper function, rename msg! => m! 2020-11-14 13:52:52 -08:00
deriv.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
doElemAsTermNotation.lean chore: move test 2020-10-31 19:19:18 -07:00
dofun_prec.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
dollarProjIssue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
doNotation1.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
doNotation2.lean feat: improve smart unfolding 2020-11-15 17:34:37 -08:00
doNotation3.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
doNotation4.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
doNotation5.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
doNotation6.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
doTrailingAtEOI.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
eagerInliningIssue.lean perf: add temporary hack for performance issue 2020-10-15 13:37:29 -07:00
elab_cmd.lean chore: fix test 2020-11-14 08:16:47 -08:00
elabCmd.lean fix: stdlib and tests 2020-11-12 07:12:30 -08:00
elabIte.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
elseIfConfusion.lean fix: do notation else if 2020-10-19 14:29:31 -07:00
emptycOverloadIssues.lean chore: fix tests 2020-10-25 09:11:13 -07:00
etaFirst.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
eval_unboxed_const.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
evalBuiltinInit.lean feat: run initializers on import 2020-10-22 11:59:55 +02:00
evalconst.lean refactor: remove MonadIO 2020-11-18 18:47:22 -08:00
expectedTypePropagation.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
explicitMotive.lean test: add explicit motive test 2020-10-23 06:00:51 -07:00
expr1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
expr_maps.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
extern.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
extmacro.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
fieldDefaultValueWithoutType.lean fix: field default value with implicit type 2020-10-22 07:02:40 -07:00
fieldIssue.lean feat: improve field notation argument search 2020-10-16 14:32:03 -07:00
finally.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
float1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
float_cases_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
float_from_bignum.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
floatarray.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
foldConsts.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
forBodyResultTypeIssue.lean chore: remove workaround 2020-11-16 16:25:58 -08:00
forInPArray.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
forInUniv.lean feat: improve smart unfolding 2020-11-15 17:34:37 -08:00
frontend1.lean refactor: remove MonadIO 2020-11-18 18:47:22 -08:00
fun.lean chore: fix tests 2020-11-10 15:45:33 -08:00
funext.lean feat: add funext tactic macro 2020-11-08 07:30:24 -08:00
generalize.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
generalizeTelescope.lean chore: use mkFreshUserName at generalizeTelescope 2020-10-31 19:19:17 -07:00
genindices.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
getline_crash.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
impByNameResolution.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
implicitTypesRecCoe.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
incmd.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
ind_cmd_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
induction1.lean feat: add repeat tactic 2020-11-03 17:20:52 -08:00
inductionTacticBug.lean fix: missing withMainMVarContext 2020-10-26 11:35:54 -07:00
inductive1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
inductive2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
inj1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
inj2.lean chore: remove unnecessary with at induction/cases tactics 2020-11-02 13:30:54 -08:00
injIssue.lean test: add injection notation test 2020-10-29 20:41:33 -07:00
inline_fn.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
inliner_loop.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
instances.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
instuniv.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
int_to_nat_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
intromacro.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
IO_test.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
irCompilerBug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
isDefEqMVarSelfIssue.lean fix: better support for constraints of the form ?m a =?= ?m b 2020-10-17 16:29:27 -07:00
kernel1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
kernel2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
kevin.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
letrecInProofs.lean chore: cleanup for presentation 2020-11-05 12:43:02 -08:00
level.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
liftMethodInMacrosIssue.lean fix: expand doIf notation before lifting nested methods 2020-10-19 11:32:51 -07:00
LiftMethodIssue.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
listDecEq.lean chore: fix tests 2020-10-25 09:11:13 -07:00
localNameResolutionWithProj.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
macro.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
macro2.lean chore: remove old notation 2020-10-26 09:16:51 -07:00
macro3.lean fix: stdlib and tests 2020-11-12 07:12:30 -08:00
macro_macro.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
macroid.lean chore: fix tests 2020-10-31 19:19:18 -07:00
match1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
matchArrayLit.lean refactor: use Lists for Array reference implementation 2020-11-17 17:05:53 -08:00
matchDiscrType.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
matcherElimUniv.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
matchNoPostponing.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
matchtac.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
meta1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
meta2.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
meta3.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
meta4.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
meta5.lean chore: add expandInterpolatedStr helper function, rename msg! => m! 2020-11-14 13:52:52 -08:00
meta6.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
meta7.lean chore: add support for reducing matchers 2020-11-15 15:07:53 -08:00
mixedMacroRules.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
mixfix.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
modAsClasses.lean feat: improve addLValArg 2020-11-12 18:59:59 -08:00
monadCache.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
monadControl.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
namespaceIssue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
nativeReflBackdoor.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
natlit.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
nested_match_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
nestedDo.lean feat: expand nested dos 2020-10-15 17:11:50 -07:00
nestedrec.lean fix: nested structural recursion 2020-10-18 10:38:51 -07:00
new_compiler.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
new_frontend2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
new_inductive.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
new_inductive2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
newfrontend1.lean fix: letDecl 2020-11-12 16:22:57 -08:00
newfrontend2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
newfrontend3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
newfrontend5.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
nicerNestedDos.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
noncomputable_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
obtain.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
optParam.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
overloaded.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
parseCore.lean chore: define notation using infix commands 2020-11-11 08:26:12 -08:00
partial1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
partialApp.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
patbug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
print_cmd.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
proofIrrelFVar.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
prv.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
ptrAddr.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
quasi_pattern_unification_approx_issue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
range.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
rc_tests.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
readerThe.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
recInfo1.lean chore: fix tests 2020-11-02 19:33:08 -08:00
reduce1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
reduce2.lean chore: fix tests 2020-10-25 09:11:13 -07:00
reduce3.lean chore: fix tests 2020-10-25 09:11:13 -07:00
Reid1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
Reparen.lean chore: define notation using infix commands 2020-11-11 08:26:12 -08:00
replace.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
resolveLVal.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
returnOptIssue.lean fix: return optional result 2020-10-20 09:33:50 -07:00
revert1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
root.lean test: _root_ 2020-11-05 15:39:22 -08:00
scc.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
sharecommon.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
spec_issue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
stateRef.lean chore: remove workarounds 2020-10-27 13:05:13 -07:00
strInterpolation.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
struct1.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
struct2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
struct3.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
struct_inst_typed.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
struct_instance_in_eqn.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
structInst.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
structInst2.lean chore: fix tests 2020-10-31 19:19:18 -07:00
structInst3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
structInst4.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
structNoBody.lean fix: optional := in the structure command 2020-10-22 04:39:20 -07:00
structuralIssue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
structuralRec1.lean feat: improve smart unfolding 2020-11-16 15:44:52 -08:00
structure.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
stxKindInsideNamespace.lean fix: SyntaxNodeKind at elab and macro commands 2020-11-05 17:20:41 -08:00
stxMacro.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
subst.lean test: add new subst tests 2020-10-23 05:39:25 -07:00
subst1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
suffices.lean feat: expand suffices macro 2020-10-27 13:05:13 -07:00
syntax1.lean feat: add ! x notation for notFollowedBy(x) in the syntax command 2020-11-17 10:57:15 -08:00
synth1.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
synthPending1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
tactic.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
tactic1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
tacticExtOverlap.lean fix: stdlib and tests 2020-11-12 07:12:30 -08:00
tacticTests.lean chore: remove unnecessary with at induction/cases tactics 2020-11-02 13:30:54 -08:00
task_test.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
task_test2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
task_test_io.lean chore: move tests to new frontend 2020-10-23 16:18:52 -07:00
termElab.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
termParserAttr.lean refactor: remove MonadIO 2020-11-18 18:47:22 -08: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 chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
trace.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
tryPureCoe.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
type_class_performance1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_append.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
typeclass_coerce.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_diamond.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_easy.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
typeclass_loop.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_metas_internal_goals1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_metas_internal_goals2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_metas_internal_goals3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_metas_internal_goals4.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
typeclass_outparam.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
ubscalar.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
unexpected_result_with_bind.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
unif_issue.lean chore: fix tests 2020-11-11 10:19:14 -08:00
unif_issue2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
univIssue.lean feat: allow universe constraints to be postponed longer 2020-10-26 15:50:05 -07:00
update.lean chore: move tests to new frontend 2020-10-23 16:18:52 -07:00
WindowsNewlines.lean fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00