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 729047b5a2 feat: auto bound implicit at constructors 
@Kha This commit adds auto bound implicits to constructors.
I was excited until I tried to define the `Bigstep` type again without
`autoBoundImplicitLocal`, and found small typos.
Example, I had
```
  | ifTrue  : eval σ₁ b = true  → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t₁ + 1)
```
where `t₁` should be `t`, but the declaration was accepted. I am
wondering whether Isabelle performs some kind of sanity checking,
and/or enforces rules such as: auto-bound implicits may only be
introduced by hypotheses.
Note that this is not an issue for definitions, because the body of
the definition will probably not type check when we have this kind of
typo in the header.
Anyway, I am putting the experiment in this branch for now.
That being said, the `Bigstep` declaration is way nicer with
`autoBoundImplicitLocal`s.

Another option is to add a new option `ctorAutoBoundImplicitLocal`
that is false by default, and activates auto implicit locals for
constructors when set to true.
2021-02-02 10:18:21 -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 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 fix: losing local instances at assertAfter 2021-01-15 19:30:03 -08:00
280.lean fix: fixes #280 2021-01-19 18:01:52 -08: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
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 feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 chore: fix tests 2020-12-28 16:27:38 -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 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: 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 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 feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
bigctor.lean fix: allow bigger ctor objects 2021-01-29 18:23:38 -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
binrel.lean feat: elaborate binrel! macro 2020-12-29 16:37:43 -08: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
casesUsing.lean test: cases-using name resolution issue 2021-02-01 13:16:19 -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: 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: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01: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: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
compiler_proj_bug.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
concatElim.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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
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 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
decidelet.lean feat: expand let-decls at decide! 2020-12-31 09:47:05 -08:00
def1.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
def2.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 feat: subsume variables under variable 2021-01-22 14:36:05 +01: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: Declaration.lean naming convention 2021-01-20 17:07:02 -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
Dorais1.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 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 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
expandAbbrevAtIsClass.lean fix: expand abbreviations at isClass? 2021-01-12 06:56:23 -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
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 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
flat_expr.lean test: reflection 2021-01-27 12:11:43 -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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
forInUniv.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
forParallel.lean feat: parallel for 2020-12-19 20:01:04 -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 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 fix: ambiguity at induction/cases 2020-11-24 14:59:12 -08:00
inductionAltExplicit.lean chore: move test without output 2021-02-02 13:37:56 +01:00
inductionTacticBug.lean fix: missing withMainMVarContext 2020-10-26 11:35:54 -07:00
inductive1.lean fix: relax eager mvar instantiation during constructor elaboration 2021-02-02 13:19:15 +01: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
infoTree.lean feat: add FieldInfo 2021-01-15 15:01:45 -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
isDefEqCheckAssignmentBug.lean fix: bug at CheckAssignment 2021-01-26 16:20:41 -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
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: subsume variables under variable 2021-01-22 14:36:05 +01: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 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: 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: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01:00
meta3.lean chore: fix typo 2020-12-28 09:01:23 -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
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 new_frontend from tests 2020-10-25 09:16:38 -07:00
monotone.lean test: implicit lambdas in action 2020-12-23 10:24:00 -08: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 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 chore: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01:00
new_frontend2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
new_inductive.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01:00
new_inductive2.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
newfrontend1.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01:00
nicerNestedDos.lean chore: remove new_frontend from tests 2020-10-25 09:16:38 -07:00
noindexAnnotation.lean feat: elaborate noindex! annotation 2020-12-28 17:49:54 -08: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 feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 feat: subsume variables under variable 2021-01-22 14:36:05 +01: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
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: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01: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: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
reduce3.lean chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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 feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01: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
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
sigmaprec.lean fix: sigma notation precedence 2020-12-26 09:35:40 -08:00
simp1.lean feat: simp infrastructure 2020-12-30 18:00:04 -08:00
simp2.lean feat: simp infrastructure 2020-12-30 18:00:04 -08:00
simp3.lean feat: simpLambda 2021-01-01 09:52:01 -08:00
simp4.lean feat: simpForall 2021-01-01 17:24:56 -08: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 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 feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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
stuckMVarBug.lean feat: subsume variables under variable 2021-01-22 14:36:05 +01: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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 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: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01: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 chore: factor out and unify common test behavior; retrieve lean from PATH 2020-05-14 14:38:52 +02:00
toExpr.lean chore: Declaration.lean naming convention 2021-01-20 17:07:02 -08: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: add options maxHeartbeats and synthInstance.maxHeartbeats 2021-01-24 17:45:50 -08:00
typeclass_diamond.lean feat: add options maxHeartbeats and synthInstance.maxHeartbeats 2021-01-24 17:45:50 -08: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 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
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
withReducibleAndInstancesCrash.lean fix: crash when using TransparencyMode.instances 2021-01-22 14:17:19 -08:00