Leonardo de Moura e74ba14f4c feat: modify structSimpleBinder parser ... @Kha It felt odd that we can write ``` map f x := ... ``` in instances, but we had to write ``` map (f x) := ... ``` when setting the field default value in a class.		2020-12-23 08:23:14 -08:00
..
.gitignore
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 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
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
1385.lean	chore: fix tests	2020-11-25 09:25:45 -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
alg.lean	refactor: more general OfNat, remove One and Zero classes	2020-12-01 07:49:52 -08:00
allGoals.lean	feat: add first tactical	2020-12-22 14:10:07 -08:00
anonymous_ctor_error_msg.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
anonymousCtor.lean
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: fix tests	2020-12-18 11:21:30 -08:00
balg.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
bigmul.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
bigop.lean	fix: adapt to new matchAlt syntax	2020-12-16 18:52:56 +01: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	chore: fix tests	2020-11-29 17:05:43 -08:00
catchThe.lean	chore: fix test	2020-12-14 10:47:44 -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	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
choiceMacroRules.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
class_inductive.lean	test: add test for issue fixed in previous commit	2020-12-05 15:50:24 -08:00
closure1.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
coeIssue1.lean	feat: simplify heuristics at propagateExpectedType	2020-11-27 12:13:29 -08: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 new_frontend from tests	2020-10-25 09:16:38 -07:00
coeSort1.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
coeSort2.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
CommandExtOverlap.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
compiler_proj_bug.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
concatElim.lean	chore: fix tests	2020-11-29 17:05:43 -08: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
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
decClassical.lean	feat: mark propDecidable as a scoped instance	2020-12-16 10:45:49 -08:00
decEq.lean	chore: cleanup	2020-12-17 18:05:53 -08: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: fix tests	2020-11-29 17:05:43 -08: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: fix tests	2020-11-25 09:25:45 -08:00
def13.lean	chore: fix tests	2020-11-29 17:05:43 -08: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	feat: heterogeneous Append experiment	2020-12-01 16:32:41 -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
derivingInhabited.lean	feat: elaborate optDeriving	2020-12-13 09:05:03 -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	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
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
elab_cmd.lean	feat: add first tactical	2020-12-22 14:10:07 -08: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
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
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
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	refactor: move to attr syntax category	2020-12-15 20:22:04 -08:00
extmacro.lean	chore: remove weird syntax sugar from macro command	2020-12-10 08:09:47 -08:00
fieldDefaultValueWithoutType.lean
fieldIssue.lean
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
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 $. notation	2020-11-19 08:47:35 -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
forParallel.lean	feat: parallel for	2020-12-19 20:01:04 -08:00
frontend1.lean	chore: remove $. notation	2020-11-19 08:47:35 -08:00
fun.lean	chore: fix tests	2020-11-25 09:25:45 -08:00
funext.lean	chore: fix tests	2020-11-29 17:05:43 -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
hmul2.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
hmulDefaultIntance.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08: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
implicitTypesRecCoe.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
incmd.lean	chore: rename syntaxMaxDepth option for consistency and discoverability	2020-12-21 16:25:01 +01:00
ind_cmd_bug.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
induction1.lean	fix: ambiguity at induction/cases	2020-11-24 14:59:12 -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
infixprio.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
inj1.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
inj2.lean	fix: ambiguity at induction/cases	2020-11-24 14:59:12 -08:00
injectionBug.lean	fix: bug at injection	2020-12-17 17:30:23 -08:00
injective.lean	test: CoeFun	2020-11-28 17:46:00 -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: fix tests	2020-12-16 10:45:27 -08:00
instanceWhere.lean	feat: add support for instance ... where	2020-11-23 18:07:02 -08: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	chore: fix tests	2020-12-18 11:21:30 -08:00
irCompilerBug.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
isDefEqIssue.lean	fix: bug at isDefEq	2020-12-02 13:27:21 -08:00
isDefEqMVarSelfIssue.lean
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
lean3_zulip_issues_1.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
letrecInProofs.lean	chore: remove $. notation	2020-11-19 08:47:35 -08:00
level.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
liftMethodInMacrosIssue.lean
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
localParsers.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
macro.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07: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
match1.lean	chore: rename syntaxMaxDepth option for consistency and discoverability	2020-12-21 16:25:01 +01:00
matchArrayLit.lean	refactor: use Lists for Array reference implementation	2020-11-17 17:05:53 -08:00
matchDiscrType.lean	chore: remove $. notation	2020-11-19 08:47:35 -08: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: fix tests	2020-11-29 17:05:43 -08:00
matrix.lean	test: matrix notation example	2020-12-21 16:40:52 -08:00
meta1.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
meta2.lean	chore: fix tests	2020-12-16 10:45:27 -08:00
meta3.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
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	test: InductiveVal.isNested	2020-12-10 14:31:40 -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 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
namespaceResolution.lean	fix: namespace resolution	2020-11-26 08:17:35 -08: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
nestedrec.lean
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	test: indentation	2020-12-22 14:53:03 -08:00
newfrontend2.lean	chore: restore correct position for match errors	2020-12-16 18:27:05 +01: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
offsetIssue.lean	feat: add [elabWithoutExpectedType] attribute	2020-11-28 13:23:37 -08:00
optParam.lean	chore: fix tests	2020-11-25 09:25:45 -08:00
overloaded.lean	feat: heterogeneous Append experiment	2020-12-01 16:32:41 -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	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
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 new_frontend from tests	2020-10-25 09:16:38 -07:00
propagateExpectedType.lean	test: propagateExpectedType	2020-11-27 12:17:23 -08: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
rational.lean	feat: add instances from coe + homogeneous operator to heterogeneous operator	2020-12-01 15:30:10 -08: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
renaming.lean	test: renaming for intrinsically typed lambda calculus	2020-11-19 19:10:49 -08:00
Reparen.lean	refactor: move Format to Init package	2020-12-18 11:21:30 -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
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
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
sharecommon.lean	refactor: heterogeneous operators	2020-12-01 14:02:46 -08:00
spec_issue.lean	chore: remove new_frontend from tests	2020-10-25 09:16:38 -07:00
specbug.lean	fix: bug at specialize.cpp	2020-12-20 17:48:46 -08: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
struct1.lean	chore: avoid Has prefix in type classes	2020-10-27 18:29:19 -07:00
struct2.lean	chore: cleaner structure/class syntax	2020-11-24 13:07:43 -08:00
struct3.lean	feat: modify structSimpleBinder parser	2020-12-23 08:23:14 -08: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	feat: optional , at structure instances	2020-11-20 15:24:34 -08:00
structNoBody.lean
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	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
stxMacro.lean	feat: only allow variables declared with mut to be reassigned	2020-11-07 17:32:13 -08:00
subst.lean
subst1.lean	chore: fix test	2020-11-27 09:00:11 -08:00
suffices.lean	chore: simplify syntax patterns using $[...]?	2020-12-09 17:06:19 -08: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	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	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
tacticTests.lean	fix: ambiguity at induction/cases	2020-11-24 14:59:12 -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	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
termElab.lean	feat: heterogeneous Append experiment	2020-12-01 16:32:41 -08:00
termParserAttr.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
test_single.sh
toExpr.lean	chore: avoid Has prefix in type classes	2020-10-27 18:29:19 -07:00
trace.lean	feat: heterogeneous Append experiment	2020-12-01 16:32:41 -08: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	feat: support for big list literals	2020-12-10 17:19:46 -08:00
typeclass_coerce.lean	feat: change synthinstance threshold	2020-12-07 10:45:08 -08: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
unifhint1.lean	feat: improve unification hints	2020-11-28 19:03:21 -08:00
unifhint2.lean	feat: optional name for unification hints	2020-11-29 08:05:26 -08:00
unifhint3.lean	feat: improve notation for setting parser names and priorities	2020-12-21 09:11:12 -08:00
unihint.lean	feat: nicer syntax for unification hints	2020-11-27 19:18:18 -08:00
univIssue.lean	feat: allow universe constraints to be postponed longer	2020-10-26 15:50:05 -07:00
update.lean
where1.lean	chore: fix tests	2020-11-29 17:05:43 -08:00
whileRepeat.lean	fix: don't change antiquotations semantics in do if	2020-12-20 17:51:37 +01:00
WindowsNewlines.lean