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 193d4dc9f5 feat: optimized deriving DecidableEq for enumeration types 
The proof term is liner on the number of constructors, but type
checking is not linear because the reduction engine in the kernel is
not efficient.
2021-09-08 16:21:32 -07:00
..
.gitignore fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +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 chore: fix test 2020-12-26 21:12:51 +01:00
108.lean chore: remove weird syntax sugar from macro command 2020-12-10 08:09:47 -08: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: fix tests 2020-12-18 11:21:30 -08:00
175.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
229.lean fix: fixes #229 2020-11-30 11:51:13 -08:00
269.lean fix: refineCore 2021-01-15 17:03:40 -08:00
270.lean chore: fix tests 2021-05-04 15:42:03 -07:00
280.lean test: add "discriminant refinement" tests 2021-03-24 19:10:50 -07:00
281.lean fix: fixes #281 2021-01-19 18:01:52 -08:00
282.lean fix: fixes #282 2021-01-19 18:01:52 -08:00
303.lean fix: fixes #303 2021-02-05 07:53:18 -08:00
305.lean feat: don't allow whitespaces between . and field name 2021-04-05 07:11:14 -07:00
310.lean fix: fixes #310 2021-02-12 18:14:42 -08:00
319.lean feat: universe level parameters in instances are outParam by default 2021-02-25 13:21:53 -08:00
326.lean chore: fix tests 2021-03-12 15:10:50 -08:00
327.lean feat: closes #327 2021-03-24 12:29:33 -07:00
329.lean fix: fixes #329 2021-03-05 13:42:54 -08:00
335.lean fix: fixes #335 2021-03-05 18:16:49 -08:00
337.lean fix: disable implicit-lambdas when elaborating patterns 2021-03-08 15:45:30 -08:00
338.lean fix: scope of forallTelescopeReducing 2021-03-08 08:29:48 -08:00
341.lean fix: add "band-aid" for #341 2021-03-10 08:11:41 -08:00
382.lean feat: use binop% to define arith operators 2021-04-30 19:40:45 -07:00
387.lean fix: issues #387 part 2 2021-04-10 15:51:07 -07:00
394.lean chore: fix tests 2021-08-07 13:22:58 -07:00
436.lean feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
436_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
441.lean test: closes #441 2021-05-15 20:37:48 -07:00
447_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
452.lean fix: fixes #452 2021-05-10 17:28:10 -07:00
457.lean fix: fixes #457 2021-05-12 20:45:54 -07:00
461a.lean feat: take auto params into account in the structure instance notation 2021-07-27 15:49:23 -07:00
461b.lean fix: bug at structure instance notation 2021-07-27 11:56:33 -07:00
462.lean feat: structure instance notation with multiple sources 2021-08-12 06:18:47 -07:00
463.lean feat: structure instance notation with multiple sources 2021-08-12 06:18:47 -07:00
470_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
471.lean fix: fixes #471 2021-05-22 15:42:52 -07:00
474_lean3.lean test: add tests for Lean3 bugs 2020-11-14 18:04:22 -08:00
481.lean fix: fixes #481 2021-05-21 20:40:26 -07:00
482.lean fix: fixes #482 2021-05-21 19:20:24 -07:00
492.lean fix: exact and refine succeed if they produce no new metavariables 2021-07-27 18:30:14 -07:00
492_lean3.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
498.lean fix: fixes #498 2021-05-31 15:42:13 -07:00
500_lean3.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
509.lean feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 2021-06-11 11:23:19 -07:00
536.lean fix: fixes #536 2021-06-29 18:24:46 -07:00
561.lean fix: make sure isDefEqOffset does not expose kernel nat literals 2021-08-02 11:27:00 -07:00
569.lean fix: add workaround to prevent code explosion at deriving for FromJson 2021-08-05 06:58:07 -07:00
602.lean fix: fixes #602 2021-08-05 16:14:04 -07:00
616.lean fix: fixes #616 2021-08-07 07:29:54 -07:00
644.lean feat: use contradiction at leaves 2021-08-22 18:41:02 -07:00
646.lean fix: work duplication bug at specialize.cpp 2021-08-27 10:35:27 -07:00
654.lean feat: optimized deriving DecidableEq for enumeration types 2021-09-08 16:21:32 -07:00
1385.lean test: add "discriminant refinement" tests 2021-03-24 19:10:50 -07: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
ac_expr.lean refactor: induction 2021-03-07 12:04:36 -08:00
alg.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
allGoals.lean fix: fixes #452 2021-05-10 17:28:10 -07:00
anonymous_ctor_error_msg.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
anonymousCtor.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
applytransp.lean chore: lean 3 behavior for apply 2021-01-05 12:29:29 -08:00
array1.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
assertAfterBug.lean fix: assertAfter 2021-02-17 13:52:43 -08:00
autoboundIssues.lean feat: refine auto bound implicit locals 2021-03-23 17:33:15 -07:00
autoLift.lean feat: add option autoLift 2021-02-19 11:02:58 -08:00
autoLiftIssue.lean feat: improve tryLiftAndCoe 2020-10-29 12:46:04 -07:00
autoparam.lean feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
backtrackable_estate.lean chore: fix tests 2020-12-18 11:21:30 -08:00
balg.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
bigctor.lean chore: disable injectivity theorems generation for big structure tests 2021-05-15 21:30:40 -07:00
bigmul.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
bigop.lean chore: fix tests 2021-08-07 13:22:58 -07:00
binderNotation.lean feat: improve mkLevelMax' 2020-11-14 08:36:23 -08:00
binrel.lean chore: fixes tests 2021-04-22 20:22:43 -07:00
binrelmacros.lean feat: use binrel! gadget to define >, <, ... notations 2020-12-29 16:53:10 -08:00
borrowBug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
calc.lean chore: fix calc test 2021-08-25 06:59:46 -07:00
calcBug.lean fix: use show .. from .. to implement calc 2021-08-29 11:33:50 -07:00
casesUsing.lean chore: fix tests 2021-08-07 13:22:58 -07:00
catchThe.lean chore: remove command universes 2021-06-29 17:01:07 -07: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 feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
choiceMacroRules.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
class_inductive.lean test: add test for issue fixed in previous commit 2020-12-05 15:50:24 -08:00
classAbbrev.lean feat: class abbrev now supports a type spec (+ test) 2021-05-20 15:23:30 -07:00
closure1.lean chore: fix tests 2021-09-07 19:14:30 -07:00
coeIssue1.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 fix: tryPureCoe? 2020-11-22 08:24:56 -08:00
coelambda.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
CoeNew.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
coeSort1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
coeSort2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
CommandExtOverlap.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
compiler_proj_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
concatElim.lean chore: fix test 2021-08-21 15:07:36 -07:00
constantCompilerBug.lean chore: fix tests 2020-11-11 10:19:14 -08:00
constFun.lean fix: Term/Sort parsers 2020-11-26 09:34:32 -08:00
constFun2.lean test: unbundled ConstantFunction 2020-11-26 09:48:12 -08:00
contra.lean test: contradiction 2021-03-03 17:13:25 -08:00
contradiction1.lean feat: contradiction catches empty inductive types 2021-03-21 21:48:43 -07:00
contradictionExfalso.lean feat: use exfalso at ElimEmptyInductive 2021-08-22 18:16:14 -07:00
contradictionLoop.lean fix: deep recursion at contradiction 2021-08-17 21:32:32 -07:00
conv1.lean feat: ignore implicit arguments at congr conv tactic 2021-09-05 09:44:52 -07:00
core.lean chore: fix tests 2021-03-10 18:45:22 -08:00
crashDiv0.lean test: div0 crash 2021-01-31 08:52:39 -08:00
csimp_type_error.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
ctorAutoParams.lean feat: auto bound implicit at constructors 2021-02-02 10:18:21 -08:00
Daniel1.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
decClassical.lean chore: fix tests 2021-08-07 13:22:58 -07:00
decEq.lean chore: cleanup 2020-12-17 18:05:53 -08:00
decidelet.lean test: use decide and nativeDecide 2021-03-11 07:46:33 -08:00
deep1.lean refactor: remove Monad Option and Alternative Option 2021-03-20 18:25:25 -07:00
def1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
def3.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def4.lean test: split tactic tests 2021-08-31 17:09:00 -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 command universes 2021-06-29 17:01:07 -07:00
def8.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
def9.lean test: add "discriminant refinement" tests 2021-03-24 19:10:50 -07:00
def10.lean test: split tactic tests 2021-08-31 17:09:00 -07:00
def11.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def12.lean chore: fix tests 2020-11-25 09:25:45 -08:00
def13.lean chore: fix tests 2021-08-07 13:22:58 -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 test: split tactic tests 2021-08-31 17:09:00 -07:00
DefEqAssignBug.lean chore: remove dead files and functions 2020-11-10 18:37:15 -08:00
depElim1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
depHd.lean feat: convert universe metavariables into parameters after elaborating theorem header 2021-02-25 16:53:58 -08:00
deriv.lean feat: force users to use discard when action result is not being bound and it is not PUnit 2020-12-08 06:14:48 -08:00
derivingBEq.lean test: mutual deriving BEq test 2020-12-18 12:36:16 -08:00
derivingHashable.lean fix: Use UInt64 in deriving handler for Hashable. 2021-06-03 06:38:44 -07:00
derivingInhabited.lean feat: elaborate optDeriving 2020-12-13 09:05:03 -08:00
derivingRpcEncoding.lean fix: deriving RpcEncoding 2021-08-01 09:58:44 +02:00
diamond1.lean feat: register instance/reducible attribute for structuer diamond coercions 2021-08-10 07:16:59 -07:00
diamond2.lean feat: improve copyNewFieldsFrom 2021-08-10 09:08:35 -07:00
diamond3.lean fix: reduce projections of expanded structures at copyDefaultValue? 2021-08-10 20:50:59 -07:00
diamond4.lean test: default value set at copied structure 2021-08-10 19:00:34 -07:00
diamond5.lean fix: structure command diamond support 2021-08-19 07:45:21 -07:00
discrRefinement.lean feat: "discriminant refinement" for match-expressions 2021-03-23 20:40:07 -07:00
discrRefinement2.lean feat: improve "discriminant refinement" 2021-03-24 21:05:08 -07:00
discrRefinement3.lean feat: new discriminant refinement procedure 2021-05-21 18:08:11 -07:00
discrTreeOffset.lean feat: add support for offset terms at DiscrTree 2021-03-14 08:23:44 -07:00
discrTreeSimp.lean feat: improve DiscrTree 2021-07-29 16:08:26 -07:00
do_eqv.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
do_eqv_proofs.lean feat: improve Lawful.lean 2021-02-23 12:38:00 -08: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 $. notation 2020-11-19 08:47:35 -08:00
doNotation1.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
doNotation2.lean fix: fixes #241 2021-05-22 19:10:07 -07:00
doNotation3.lean chore: fix tests 2021-08-07 13:22:58 -07:00
doNotation4.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
doNotation5.lean chore: fix tests 2021-03-11 11:35:51 -08:00
doNotation6.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
Dorais1.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
dotNotationRecDecl.lean feat: do not consider dot notation when isAuxDecl is true 2021-08-21 16:35:32 -07:00
doTrailingAtEOI.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
eagerInliningIssue.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
elab_cmd.lean fix: fixes #452 2021-05-10 17:28:10 -07:00
elabCmd.lean feat: macro: use appropriate antiquotation kind dependent on bound syntax 2020-12-14 13:54:34 +01:00
elabIte.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
elseCaseArrow.lean fix: doLetArrow and doReassignArrow 2020-11-26 10:29:08 -08:00
elseIfConfusion.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
emptycOverloadIssues.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
evalconst.lean refactor: remove MonadIO 2020-11-18 18:47:22 -08:00
evalProp.lean feat: allow (decidable) propositions at #eval 2021-08-27 15:06:48 -07:00
exp.lean feat: nary generalize tactic 2021-08-30 16:31:39 -07:00
expandAbbrevAtIsClass.lean chore: fix tests 2021-03-12 15:10:50 -08:00
expectedTypePropagation.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
explicitMotive.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
explictOpenDeclIssue.lean fix: issue raised by Andrew 2021-04-12 10:51:44 -07:00
expr1.lean chore: fix tests 2021-09-07 19:14:30 -07:00
expr_maps.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
extern.lean refactor: move to attr syntax category 2020-12-15 20:22:04 -08:00
extmacro.lean feat: add trivial extensible (macro) tactic 2021-03-24 09:50:56 -07:00
falseElimAtSimpLocalDecl.lean feat: use False.elim when simplifying local declarations that rewrite to False 2021-03-17 15:30:54 -07:00
fieldAbbrevInPat.lean feat: add macro for expanding field abbrev notation 2021-08-11 16:02:50 -07:00
fieldAutoBound.lean test: for field auto implicit bound feature 2021-02-20 07:52:42 -08:00
fieldDefaultValueWithoutType.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
fieldIssue.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
finally.lean feat: force users to use discard when action result is not being bound and it is not PUnit 2020-12-08 06:14:48 -08:00
finLit.lean feat: ignore nested proofs in patterns 2021-09-05 15:46:03 -07:00
flat_expr.lean refactor: induction 2021-03-07 12:04:36 -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 when and «unless» 2021-03-20 18:52:18 -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 command universes 2021-06-29 17:01:07 -07:00
forInPArray.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
forInUniv.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
forParallel.lean feat: parallel for 2020-12-19 20:01:04 -08:00
french_quote.lean feat: Lean 3 french single quote notation 2021-03-04 09:43:59 -08:00
fun.lean chore: fix tests 2020-11-25 09:25:45 -08:00
funext.lean chore: fix tests 2021-03-11 10:51:11 -08:00
funMatchIssue.lean fix: issue at expandMatchAlts 2021-03-30 12:55:59 -07:00
generalize.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
generalizeMany.lean feat: nary generalize tactic 2021-08-30 16:31:39 -07:00
generalizeTelescope.lean chore: fix tests 2021-03-10 18:45:22 -08:00
genindices.lean chore: fix tests 2021-03-10 18:45:22 -08:00
getline_crash.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
haveDestruct.lean feat: have ... := ... syntax closer to let 2021-05-06 15:38:57 -07:00
hmul2.lean chore: fix tests 2021-03-11 10:51:11 -08:00
hmulDefaultIntance.lean refactor: heterogeneous operators 2020-12-01 14:02:46 -08:00
ifcongr.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
ifThenElseIssue.lean fix: if-then-else elaboration issue 2020-11-21 20:51:28 -08:00
impByNameResolution.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
impLambdaTac.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
implicitApplyIssue.lean chore: fixes tests 2021-04-22 20:22:43 -07:00
implicitTypesRecCoe.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
incmd.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
ind_cmd_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
induction1.lean feat: improve generalizing at induction 2021-03-27 14:28:03 -07:00
inductionAltExplicit.lean chore: fix mkForbiddenSet 2021-03-27 14:59:05 -07:00
inductionTacticBug.lean fix: missing withMainMVarContext 2020-10-26 11:35:54 -07:00
inductive1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
inductive2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
inductive_pred.lean refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 2021-06-06 06:40:09 -07:00
infixprio.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
inj1.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
inj2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
injectionBug.lean fix: bug at injection 2020-12-17 17:30:23 -08:00
injections1.lean test: missing tests 2021-09-08 08:00:36 -07:00
injective.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
injIssue.lean test: add injection notation test 2020-10-29 20:41:33 -07:00
injSimp.lean feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
inline_fn.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
inlineLoop.lean fix: inline loop 2021-02-04 17:17:51 -08:00
inliner_loop.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
instances.lean chore: fix tests 2020-12-16 10:45:27 -08:00
instanceWhere.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
instprio.lean feat: add optional (priority := <prio>) to instance command 2020-12-21 10:02:12 -08: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 fix: change IO.FS.Handle.read to return empty array at EOF 2021-06-08 13:17:53 +02:00
ioRandomBytes.lean feat: IO.getRandomBytes 2021-07-24 10:45:28 +02:00
irCompilerBug.lean refactor: remove Monad Option and Alternative Option 2021-03-20 18:25:25 -07:00
isDefEqCheckAssignmentBug.lean chore: throwError! => throwError, throwErrorAt! => throwErrorAt 2021-03-11 11:59:45 -08:00
isDefEqIssue.lean fix: bug at isDefEq 2020-12-02 13:27:21 -08:00
isDefEqMVarSelfIssue.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
jason1.lean fix: scope of forallTelescopeReducing 2021-03-08 08:29:48 -08: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
KyleAlg.lean feat: injectivity theorems for types defined in the prelude 2021-05-14 18:32:26 -07:00
KyleAlgAbbrev.lean feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
lean3_zulip_issues_1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
lemma.lean feat: parser alias for 'declVal' 2021-04-12 16:59:54 -07:00
letrecInProofs.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
level.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
liftMethodInMacrosIssue.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
LiftMethodIssue.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
listDecEq.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
localNameResolutionWithProj.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
localParsers.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
macro.lean chore: fix test 2021-03-31 21:24:28 +02:00
macro2.lean chore: remove $. notation 2020-11-19 08:47:35 -08:00
macro3.lean chore: adapt stdlib to new antiquotation splices 2020-12-12 17:20:03 +01:00
macro_macro.lean chore: remove weird syntax sugar from macro command 2020-12-10 08:09:47 -08:00
macroid.lean chore: restore correct position for match errors 2020-12-16 18:27:05 +01:00
macroParams.lean feat: revise macro parameter syntax 2021-08-12 07:48:42 -07:00
manyAritySyntax.lean feat: add enum command for declaring enumeration types 2021-09-05 16:58:49 -07:00
mapTR.lean test: add mapTR test 2021-08-22 16:51:38 -07:00
match1.lean fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true 2021-08-17 21:32:32 -07:00
match_unit.lean fix: matchUnit simplification 2021-02-19 13:51:08 -08:00
matchArrayLit.lean chore: fix tests 2021-08-07 13:22:58 -07:00
matchDiscrType.lean chore: remove $. notation 2020-11-19 08:47:35 -08:00
matchEqs.lean feat: add simpMatch and use it at splitMatch 2021-08-31 12:53:41 -07:00
matchEqsBug.lean feat: add environment extension for storing match conditional equations and splitter 2021-08-28 14:49:20 -07:00
matcherElimUniv.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
matchGenBug.lean fix: match generalization bug 2021-04-19 18:37:25 -07:00
matchGenIssue.lean fix: improve match generalizing feature 2021-04-26 19:22:03 -07:00
matchNoPostponing.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
matchRw.lean feat: allow user to define rewrite lemmas with (local) match expressions 2021-02-19 15:18:19 -08:00
matchtac.lean feat: match auto generalization 2021-04-16 21:48:38 -07:00
matchUnifyBug.lean fix: missing whnf at Unify.unify 2021-03-21 22:38:46 -07:00
matchVarIssue.lean fix: simple match case 2021-03-24 11:46:55 -07:00
matchWithSearch.lean chore: remove unnecessary annotations 2021-03-23 20:42:59 -07:00
mathport18.lean test: mathport issue https://github.com/dselsam/mathport/issues/18 2021-08-15 08:11:20 -07:00
mathport_issue16.lean feat: add instance from CoeSort to CoeTail 2021-08-18 20:24:43 -07:00
matrix.lean chore: fix tests 2021-08-07 13:22:58 -07:00
meta.lean chore: example 2021-04-12 16:56:10 -07:00
meta1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
meta2.lean fix: make sure isDefEqOffset does not expose kernel nat literals 2021-08-02 11:27:00 -07:00
meta3.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta4.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta5.lean chore: fix tests 2021-09-07 19:14:30 -07:00
meta6.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
meta7.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
methodsRetInhabited.lean refactor: revert MonadRef changes 2021-06-21 10:17:26 -07:00
Miller1.lean test: TC issue repro 2021-01-13 18:41:01 -08:00
missingDeclName.lean fix: missing withDeclName 2021-01-11 06:50:55 -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: fix test 2020-12-06 19:00:24 -08:00
monadControl.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
monotone.lean chore: fixes tests 2021-04-22 20:22:43 -07:00
mulcomm.lean fix: instance + where + implicts issue 2021-04-24 20:07:35 -07:00
multiTargetCasesInductionIssue.lean feat: nary generalize tactic 2021-08-30 16:31:39 -07:00
namespaceIssue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
namespaceResolution.lean fix: namespace resolution 2020-11-26 08:17:35 -08:00
nativeReflBackdoor.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
nestedInductiveIssue.lean fix: eta-expanded term at levelMVarToParam 2021-01-22 14:17:19 -08:00
nestedrec.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
new_compiler.lean refactor: separate pp.funBinderTypes and pp.piBinderTypes 2021-08-09 16:13:40 +02:00
new_frontend2.lean chore: fix tests 2021-03-11 10:51:11 -08:00
new_inductive.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
new_inductive2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
newfrontend1.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
newfrontend2.lean fix: make the match behavior more uniform 2021-03-30 12:19:31 -07:00
newfrontend3.lean chore: fix tests 2021-08-07 13:22:58 -07:00
newfrontend5.lean chore: fix tests 2021-03-11 10:51:11 -08:00
nicerNestedDos.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
noindexAnnotation.lean chore: fix tests 2021-08-07 13:22:58 -07:00
noncomputable_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
nonrec.lean feat: elaborate nonrec modifier 2021-08-21 17:02:54 -07:00
obtain.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
offsetIssue.lean chore: fix tests 2021-03-12 15:10:50 -08:00
ofNatNormNum.lean feat: convert "orphan" kernel nat literals n into ofNat n 2021-09-08 14:58:13 -07:00
openInScopeBug.lean chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
openTermTactic.lean feat: open in terms and tatics 2021-03-06 15:33:00 -08:00
optParam.lean chore: add workarounds 2021-03-23 18:35:27 -07:00
Ord.lean test: add test that deriving Ord compiles in various cases. 2021-04-03 21:27:26 -07:00
overloaded.lean feat: heterogeneous Append experiment 2020-12-01 16:32:41 -08:00
panicAtCheckAssignment.lean chore: throwError! => throwError, throwErrorAt! => throwErrorAt 2021-03-11 11:59:45 -08:00
parsePrelude.lean feat: force users to use discard when action result is not being bound and it is not PUnit 2020-12-08 06:14:48 -08:00
parserAliasShadow.lean fix: name resolution at syntax command 2020-12-22 08:40:00 -08:00
partial1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
partialApp.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
patbug.lean chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
pendingInstBug.lean test: lost synthetic mvar issue 2021-02-20 13:01:36 -08:00
pendingMVarIssue.lean fix: pending metavariable issue 2021-08-10 14:52:53 -07:00
PPTopDownAnalyze.lean feat: pp.analyze improve heuristics for fun binders 2021-08-12 09:37:57 +02:00
precDSL.lean fix: handle prec DSL at infixl macro 2020-12-14 15:35:37 -08:00
print_cmd.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
prioDSL.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
proofIrrelFVar.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
propagateExpectedType.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
quotInd.lean test: for induction q with Quot.ind issue 2021-08-26 11:15:14 -07:00
range.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
rational.lean test: use decide and nativeDecide 2021-03-11 07:46:33 -08:00
rc_tests.lean feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
readerThe.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
recInfo1.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
reduce1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
reduce2.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
reduce3.lean chore: fix tests 2021-08-07 13:22:58 -07:00
reductionBug.lean fix: bug at reduceRec 2021-05-07 14:21:37 -07:00
reflectiveIndPred.lean chore: rename ProofBelow to below. 2021-04-26 20:33:21 +02:00
Reid1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
renameI.lean feat: add renameI tactic 2021-08-25 18:50:59 -07:00
renaming.lean test: renaming for intrinsically typed lambda calculus 2020-11-19 19:10:49 -08:00
Reparen.lean chore: fix tests 2021-08-06 14:05:00 -07: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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
rw_inst_mvars.lean fix: instantiate mvars in rewrite tactic 2021-06-11 10:27:05 -07:00
scc.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
scopedCommandAfterOpen.lean fix: update tokenTable at withNamespace parser combinator 2021-08-23 09:41:36 -07:00
scopedParsers.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
scopedParsers2.lean test: scoped parser after open 2020-12-05 08:35:30 -08:00
secVarBug.lean fix: make sure the resulting array size is equal to the number of binders 2021-05-04 19:46:14 -07:00
set.lean test: use decide and nativeDecide 2021-03-11 07:46:33 -08:00
setOptionTermTactic.lean fix: make sure simp only still uses eq_self 2021-08-30 09:50:11 -07:00
sharecommon.lean refactor: heterogeneous operators 2020-12-01 14:02:46 -08:00
sigmaprec.lean fix: sigma notation precedence 2020-12-26 09:35:40 -08:00
simp1.lean chore: throwError! => throwError, throwErrorAt! => throwErrorAt 2021-03-11 11:59:45 -08:00
simp2.lean feat: simp infrastructure 2020-12-30 18:00:04 -08:00
simp3.lean chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
simp4.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
simp5.lean chore: add basic simp lemmas 2021-02-15 11:32:19 -08:00
simp6.lean feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
simp7.lean refactor: define Nat.le using inductive type 2021-08-20 19:39:45 -07:00
simp_all.lean feat: add simp_all tactic 2021-03-19 22:34:35 -07:00
simp_all_contextual.lean feat: contextual := true at simp_all 2021-03-24 15:49:31 -07:00
simpBug.lean fix: using incorrect local context to process simp arguments 2021-08-26 12:49:12 -07:00
simpCondLemma.lean chore: add basic simp lemmas 2021-02-15 11:32:19 -08:00
simpDefToUnfold.lean feat: allow users to mark definitions with [simp] 2021-03-17 19:11:55 -07:00
simpDischargeLoop.lean fix: missing withoutModifyingState at elabSimpConfig 2021-05-16 13:07:13 -07:00
simpImpLocal.lean fix: local simp lemmas with implicits 2021-02-20 14:29:15 -08:00
simpInv.lean feat: elaborate <- modifier at simp arguments 2021-08-15 07:07:58 -07:00
simpMatchDiscr.lean feat: support for simplifying match discriminants 2021-03-16 15:51:36 -07:00
simpOnly.lean fix: make sure simp only still uses eq_self 2021-08-30 09:50:11 -07:00
simpPreprocess.lean feat: add simp lemma preprocessor 2021-03-09 19:16:14 -08:00
simpRwBug.lean fix: missing whnf at tryLemma? 2021-08-30 08:33:58 -07:00
simpStar.lean feat: elaborate * simp argument 2021-08-15 08:02:21 -07:00
simpStarHyp.lean fix: location notation and simp 2021-03-19 19:54:22 -07:00
sizeof1.lean feat: finish sizeOf_spec lemma generation 2021-01-27 17:20:23 -08:00
sizeof2.lean test: inductive types for testing SizeOf.lean 2021-01-27 16:26:03 -08:00
sizeof3.lean feat: finish sizeOf_spec lemma generation 2021-01-27 17:20:23 -08:00
sizeof4.lean test: inductive types for testing SizeOf.lean 2021-01-27 16:26:03 -08:00
sizeof5.lean test: inductive types for testing SizeOf.lean 2021-01-27 16:26:03 -08:00
sizeof6.lean fix: use previously generated sizeOf_spec lemmas to expand rhs 2021-01-27 18:14:25 -08:00
spec_issue.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
specbug.lean test: use decide and nativeDecide 2021-03-11 07:46:33 -08:00
specialize1.lean feat: add specialize tactic 2021-09-08 08:00:02 -07:00
split1.lean feat: add simpMatch and use it at splitMatch 2021-08-31 12:53:41 -07:00
split2.lean test: split tactic 2021-08-31 13:14:10 -07:00
split3.lean test: missing tests 2021-09-08 08:00:36 -07:00
stateRef.lean chore: remove $. notation 2020-11-19 08:47:35 -08:00
strInterpolation.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
strLitProj.lean fix: projection of string literals 2021-05-07 14:38:21 -07:00
struct1.lean chore: avoid Has prefix in type classes 2020-10-27 18:29:19 -07:00
struct2.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
struct3.lean test: add *> laziness test 2021-09-07 18:03:15 -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 some tests 2021-09-07 17:20:21 -07:00
structInst3.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
structInst4.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
structNoBody.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
structPrivateFieldBug.lean fix: private field + default value bug 2021-08-09 19:01:08 -07:00
structPrivateFieldBug2.lean test: overriding default value of private field 2021-08-09 19:01:08 -07:00
structuralIssue.lean refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
structuralIssue2.lean fix: improve structural recursion 2021-04-13 10:31:43 -07:00
structuralRec1.lean fix: deal with params for inductive predicates. 2021-06-06 06:40:09 -07:00
structure.lean Feat: Add getAllParentStructures 2021-04-07 18:06:10 -07:00
stuckMVarBug.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
stxKindInsideNamespace.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
stxMacro.lean feat: only allow variables declared with mut to be reassigned 2020-11-07 17:32:13 -08:00
subst.lean chore: fix tests 2021-08-07 13:22:58 -07:00
subst1.lean chore: fix test 2020-11-27 09:00:11 -08:00
subtype_inj.lean fix: Injection.lean 2021-01-30 11:58:56 -08:00
suffices.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
syntax1.lean feat: add ! x notation for notFollowedBy(x) in the syntax command 2020-11-17 10:57:15 -08:00
syntaxPrio.lean feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
synth1.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
synthPending1.lean chore: fix tests 2021-08-07 13:22:58 -07:00
synthPendingBug.lean fix: synthPending bug 2021-08-04 20:07:06 -07:00
tactic.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
tactic1.lean chore: add sorry tactic 2021-09-08 08:10:37 -07:00
tacticExtOverlap.lean chore: enforce notation parameter naming convention 2021-04-19 18:54:09 -07:00
tacticTests.lean fix: induction/cases: accept wildcard alternative even if some (but not all) cases have been excluded 2021-05-06 14:28:00 +02:00
task_test.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
task_test2.lean chore: fix tests 2021-03-11 11:35:51 -08:00
task_test_io.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
tcUnivIssue.lean fix: TC issue introduced by recent bug fix 2021-08-23 17:32:19 -07:00
termElab.lean feat: heterogeneous Append experiment 2020-12-01 16:32:41 -08:00
termParserAttr.lean chore: remove when and «unless» 2021-03-20 18:52:18 -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 chore: remove when and «unless» 2021-03-20 18:52:18 -07:00
toFromJson.lean chore: fix test 2021-08-05 06:27:57 -07:00
trace.lean perf: make trace[...] ... notation lazy 2021-06-23 00:07:27 -07:00
traceElabIssue.lean fix: tolerate type incorrect terms 2021-04-29 21:34:15 -07:00
trans.lean chore: fix test 2021-08-25 07:00:25 -07:00
tryHeuristicPerfIssue.lean feat: add basic isDefEq cache 2021-07-28 16:29:44 -07:00
tryHeuristicPerfIssue2.lean feat: add basic isDefEq cache 2021-07-28 16:29:44 -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
typeAscImp.lean feat: type ascription should disable implicit lambdas 2021-05-12 19:29:36 -07:00
typeclass_append.lean feat: support for big list literals 2020-12-10 17:19:46 -08:00
typeclass_coerce.lean chore: increase threshold for Windows workaround in the previous commit 2021-05-15 21:15:37 -07:00
typeclass_diamond.lean chore: increase threshold for Windows workaround in the previous commit 2021-05-15 21:15:37 -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
unifhint1.lean feat: improve unification hints 2020-11-28 19:03:21 -08:00
unifhint2.lean chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
unifhint3.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
unihint.lean chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
univIssue.lean chore: remove command universes 2021-06-29 17:01:07 -07:00
update.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
where1.lean chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
whileRepeat.lean chore: use polymorphic method forIn 2021-02-04 18:13:01 -08:00
whnfDelayedMVarIssue.lean fix: whnfCore not expanding delayed assignments 2021-02-05 15:14:12 -08:00
WindowsNewlines.lean fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00
withReducibleAndInstancesCrash.lean chore: fix tests 2021-03-10 18:45:22 -08:00