max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean
History
Sebastian Ullrich 0bd864deca fix: nesting of pattern info nodes
2022-06-27 22:37:02 +02:00
..
interactive feat: show term goal at end of term as well 2022-06-23 14:44:19 +02:00
Reformat chore: fix tests 2022-06-16 23:33:57 +02:00
run feat: dot notation and aliases 2022-06-27 12:42:25 -07:00
server fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00
trust0 fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00
.gitignore
217.lean
217.lean.expected.out
220.lean
220.lean.expected.out
223.lean
223.lean.expected.out
236.lean
236.lean.expected.out
241.lean
241.lean.expected.out
242.lean
242.lean.expected.out
243.lean
243.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
247.lean
247.lean.expected.out
248.lean chore: fix tests 2022-06-14 17:27:13 -07:00
248.lean.expected.out chore: fix tests 2022-06-14 17:27:13 -07:00
255.lean
255.lean.expected.out feat: improve the heuristic for notation delab 2022-06-23 13:27:53 -07:00
276.lean
276.lean.expected.out
277a.lean
277a.lean.expected.out
277b.lean
277b.lean.expected.out
283.lean
283.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
297.lean
297.lean.expected.out
301.lean
301.lean.expected.out fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
302.lean
302.lean.expected.out
307.lean
307.lean.expected.out
309.lean
309.lean.expected.out
331.lean
331.lean.expected.out
343.lean fix: universe level parameter stabilitity issue 2022-06-10 14:08:08 -07:00
343.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
345.lean
345.lean.expected.out
346.lean
346.lean.expected.out
348.lean
348.lean.expected.out
353.lean
353.lean.expected.out feat: backtrack when applying default instances if subproblems cannot be solved 2022-05-07 09:56:38 -07:00
361.lean
361.lean.expected.out
366.lean
366.lean.expected.out
386.lean
386.lean.expected.out
389.lean
389.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
414.lean
414.lean.expected.out
415.lean
415.lean.expected.out
421.lean
421.lean.expected.out
423.lean
423.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
435.lean
435.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
435b.lean
435b.lean.expected.out
439.lean
439.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
440.lean
440.lean.expected.out
445.lean
445.lean.expected.out
448.lean
448.lean.expected.out
449.lean
449.lean.expected.out
450.lean
450.lean.expected.out
456.lean
456.lean.expected.out
469.lean
469.lean.expected.out
474.lean
474.lean.expected.out
490.lean fix: _root_ prefix in declarations 2022-06-13 14:03:18 -07:00
490.lean.expected.out fix: _root_ prefix in declarations 2022-06-13 14:03:18 -07:00
496.lean
496.lean.expected.out
529.lean
529.lean.expected.out
550.lean
550.lean.expected.out
586.lean
586.lean.expected.out
593.lean
593.lean.expected.out
603.lean
603.lean.expected.out
604.lean
604.lean.expected.out
620.lean
620.lean.expected.out
621.lean
621.lean.expected.out
625.lean
625.lean.expected.out
629.lean
629.lean.expected.out
641.lean
641.lean.expected.out
653.lean
653.lean.expected.out
655.lean
655.lean.expected.out
679.lean
679.lean.expected.out
689.lean
689.lean.expected.out
690.lean
690.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
697.lean
697.lean.expected.out
714.lean
714.lean.expected.out
755.lean
755.lean.expected.out
770.lean
770.lean.expected.out
799.lean
799.lean.expected.out
801.lean
801.lean.expected.out
813.lean
813.lean.expected.out
815b.lean
815b.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
906.lean
906.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
916.lean
916.lean.expected.out
948.lean
948.lean.expected.out fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
951.lean
951.lean.expected.out
973.lean
973.lean.expected.out
973b.lean chore: fix tests 2022-06-14 16:43:22 -07:00
973b.lean.expected.out fix: remove check from Simp.synthesizeArgs 2022-06-03 07:40:30 -07:00
974.lean
974.lean.expected.out
986.lean
986.lean.expected.out
995.lean
995.lean.expected.out
1007.lean
1007.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
1011.lean
1011.lean.expected.out
1018unknowMVarIssue.lean
1018unknowMVarIssue.lean.expected.out fix: nesting of pattern info nodes 2022-06-27 22:37:02 +02:00
1021.lean
1021.lean.expected.out chore: use let/if in do blocks 2022-06-13 17:10:14 -07:00
1026.lean
1026.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
1027.lean
1027.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
1038.lean
1038.lean.expected.out
1039.lean
1039.lean.expected.out
1050.lean
1050.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
1057.lean
1057.lean.expected.out
1062.lean
1062.lean.expected.out
1074a.lean
1074a.lean.expected.out
1074b.lean
1074b.lean.expected.out chore: fix tests 2022-05-31 18:17:56 -07:00
1079.lean
1079.lean.expected.out
1081.lean
1081.lean.expected.out
1098.lean
1098.lean.expected.out
1112.lean
1112.lean.expected.out
1113.lean feat: apply rfl theorems at dsimp 2022-04-21 16:26:57 -07:00
1113.lean.expected.out feat: apply rfl theorems at dsimp 2022-04-21 16:26:57 -07:00
1163.lean fix: generate sorry warning only if there are no error messages 2022-06-01 06:32:05 -07:00
1163.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
1206.lean fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
1206.lean.expected.out fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
1235.lean fix: remove kabstractWithPred 2022-06-20 16:35:18 -07:00
1235.lean.expected.out fix: remove kabstractWithPred 2022-06-20 16:35:18 -07:00
1240.lean fix: fixes #1240 2022-06-23 05:53:06 -07:00
1240.lean.expected.out fix: fixes #1240 2022-06-23 05:53:06 -07:00
abst.lean
abst.lean.expected.out
allFieldForConstants.lean feat: save mutual block information for definitions/theorems/opaques 2022-06-23 16:39:51 -07:00
allFieldForConstants.lean.expected.out feat: save mutual block information for definitions/theorems/opaques 2022-06-23 16:39:51 -07:00
ambiguousOpenExport.lean feat: report error on ambiguous export and open commands 2022-06-17 09:58:36 -07:00
ambiguousOpenExport.lean.expected.out feat: report error on ambiguous export and open commands 2022-06-17 09:58:36 -07:00
antiquotRecovery.lean fix: skip antiquotations during parser recovery 2022-04-27 10:41:27 +02:00
antiquotRecovery.lean.expected.out fix: skip antiquotations during parser recovery 2022-04-27 10:41:27 +02:00
appParserIssue.lean
appParserIssue.lean.expected.out
argNameAtPlaceholderError.lean
argNameAtPlaceholderError.lean.expected.out
argNameIfMacroScopes.lean
argNameIfMacroScopes.lean.expected.out
arrayGetU.lean
arrayGetU.lean.expected.out
attrCmd.lean
attrCmd.lean.expected.out
autobound_and_macroscopes.lean
autobound_and_macroscopes.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
autoBoundErrorMsg.lean
autoBoundErrorMsg.lean.expected.out
autoBoundImplicits1.lean
autoBoundImplicits1.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
autoBoundImplicits2.lean
autoBoundImplicits2.lean.expected.out
autoBoundPostponeLoop.lean
autoBoundPostponeLoop.lean.expected.out
autoImplicitChain.lean
autoImplicitChain.lean.expected.out
autoImplicitChainNameIssue.lean
autoImplicitChainNameIssue.lean.expected.out
autoImplicitCtorParamIssue.lean fix: auto implicit behavior on constructors 2022-05-04 15:04:49 -07:00
autoImplicitCtorParamIssue.lean.expected.out fix: auto implicit behavior on constructors 2022-05-04 15:04:49 -07:00
autoImplicitForbidden.lean feat: refine auto bound implicit feature 2022-04-21 10:17:15 -07:00
autoImplicitForbidden.lean.expected.out feat: refine auto bound implicit feature 2022-04-21 10:17:15 -07:00
autoIssue.lean
autoIssue.lean.expected.out
autoPPExplicit.lean
autoPPExplicit.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
auxDeclIssue.lean
auxDeclIssue.lean.expected.out
badBinderName.lean
badBinderName.lean.expected.out
badIhName.lean
badIhName.lean.expected.out
beginEndAsMacro.lean
beginEndAsMacro.lean.expected.out
bigUnivOffsets.lean
bigUnivOffsets.lean.expected.out
binderCacheIssue.lean
binderCacheIssue.lean.expected.out
binderCacheIssue2.lean
binderCacheIssue2.lean.expected.out
bindersAbstractingUnassignedMVars.lean
bindersAbstractingUnassignedMVars.lean.expected.out
binomialHeap.lean
binomialHeap.lean.expected.out
binop_lazy.lean
binop_lazy.lean.expected.out
binopIssues.lean
binopIssues.lean.expected.out
binrel_binop.lean feat: improve binrel% elaborator 2022-05-09 18:39:52 -07:00
binrel_binop.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
binsearch.lean
binsearch.lean.expected.out
bintreeGoal.lean
bintreeGoal.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
bitwise.lean
bitwise.lean.expected.out
byCasesMetaM.lean
byCasesMetaM.lean.expected.out
bytearray.lean
bytearray.lean.expected.out
cacheIssue.lean
cacheIssue.lean.expected.out
calcErrors.lean
calcErrors.lean.expected.out
cdotAtSimpArg.lean
cdotAtSimpArg.lean.expected.out
cdotTuple.lean
cdotTuple.lean.expected.out
class_def_must_fail.lean
class_def_must_fail.lean.expected.out
classBadOutParam.lean
classBadOutParam.lean.expected.out
collectDepsIssue.lean
collectDepsIssue.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
commandPrefix.lean
commandPrefix.lean.expected.out
congrThmIssue.lean
congrThmIssue.lean.expected.out fix: regression reported at issue #1113 2022-04-23 15:39:04 -07:00
constDelab.lean
constDelab.lean.expected.out
constructorTac.lean
constructorTac.lean.expected.out
consumePPHint.lean chore: fix tests 2022-06-14 16:43:22 -07:00
consumePPHint.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
conv1.lean feat: allow conv mode's arg command to access implicit arguments 2022-06-14 16:15:38 -07:00
conv1.lean.expected.out feat: allow conv mode's arg command to access implicit arguments 2022-06-14 16:15:38 -07:00
convInConv.lean
convInConv.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
convPatternAtLetIssue.lean
convPatternAtLetIssue.lean.expected.out fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
convPatternMatchIssue.lean
convPatternMatchIssue.lean.expected.out fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
convZetaLetExt.lean feat: allow ext conv tactic to go inside let-declarations 2022-06-22 19:27:04 -07:00
convZetaLetExt.lean.expected.out feat: allow ext conv tactic to go inside let-declarations 2022-06-22 19:27:04 -07:00
copy-produced
csimpAttr.lean
csimpAttr.lean.expected.out
csimpAttrAppend.lean
csimpAttrAppend.lean.expected.out
ctor_layout.lean
ctor_layout.lean.expected.out
ctorUnivTooBig.lean
ctorUnivTooBig.lean.expected.out
dbgMacros.lean
dbgMacros.lean.expected.out
decimals.lean
decimals.lean.expected.out
decreasing_by.lean
decreasing_by.lean.expected.out
defaultInstance.lean
defaultInstance.lean.expected.out
defaultInstanceWithPrio.lean
defaultInstanceWithPrio.lean.expected.out
defInst.lean
defInst.lean.expected.out chore: fix tests 2022-05-31 18:17:56 -07:00
delabUnexpand.lean
delabUnexpand.lean.expected.out
delta.lean
delta.lean.expected.out
derivingDecidableEq.lean feat: support proofs in deriving DecidableEq 2022-05-30 07:36:30 -07:00
derivingDecidableEq.lean.expected.out feat: support proofs in deriving DecidableEq 2022-05-30 07:36:30 -07:00
derivingRepr.lean
derivingRepr.lean.expected.out
diamond1.lean
diamond1.lean.expected.out
diamond2.lean
diamond2.lean.expected.out
diamond3.lean
diamond3.lean.expected.out
diamond4.lean
diamond4.lean.expected.out
diamond5.lean
diamond5.lean.expected.out
diamond6.lean
diamond6.lean.expected.out
diamond7.lean
diamond7.lean.expected.out
diamond8.lean
diamond8.lean.expected.out
diamond9.lean
diamond9.lean.expected.out
diamond10.lean
diamond10.lean.expected.out
docStr.lean
docStr.lean.expected.out
doErrorMsg.lean fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
doErrorMsg.lean.expected.out fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
doIfLet.lean
doIfLet.lean.expected.out
doIssue.lean
doIssue.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
doLetLoop.lean
doLetLoop.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
doNotation1.lean
doNotation1.lean.expected.out
doSeqRightIssue.lean
doSeqRightIssue.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
eagerCoeExpansion.lean
eagerCoeExpansion.lean.expected.out
eagerUnfoldingIssue.lean feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
eagerUnfoldingIssue.lean.expected.out feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
elseifDoErrorPos.lean
elseifDoErrorPos.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
emptyc.lean
emptyc.lean.expected.out
eoi.lean
eoi.lean.expected.out
eqValue.lean
eqValue.lean.expected.out
eraseInsts.lean
eraseInsts.lean.expected.out
eraseSimp.lean
eraseSimp.lean.expected.out
errorOnInductionForNested.lean
errorOnInductionForNested.lean.expected.out
errorRecoveryBug.lean
errorRecoveryBug.lean.expected.out
eta.lean
eta.lean.expected.out
etaStructIssue.lean
etaStructIssue.lean.expected.out
eval_except.lean
eval_except.lean.expected.out
evalInstMessage.lean
evalInstMessage.lean.expected.out
evalSorry.lean
evalSorry.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
evalWithMVar.lean
evalWithMVar.lean.expected.out
exactErrorPos.lean
exactErrorPos.lean.expected.out
exitAfterParseError.lean
exitAfterParseError.lean.expected.out
extract.lean
extract.lean.expected.out
failTac.lean
failTac.lean.expected.out
file_not_found.lean
file_not_found.lean.expected.out
filePath.lean
filePath.lean.expected.out
fixedIndexToParamIssue.lean
fixedIndexToParamIssue.lean.expected.out
fixedIndicesToParams.lean
fixedIndicesToParams.lean.expected.out
forallMetaBounded.lean
forallMetaBounded.lean.expected.out
forErrors.lean
forErrors.lean.expected.out
Format.lean
Format.lean.expected.out
funExpected.lean
funExpected.lean.expected.out
funInfoBug.lean
funInfoBug.lean.expected.out
funParen.lean
funParen.lean.expected.out
gcd.lean
gcd.lean.expected.out
have.lean
have.lean.expected.out
heapSort.lean
heapSort.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
hidingInaccessibleNames.lean
hidingInaccessibleNames.lean.expected.out
holeErrors.lean feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided 2022-06-02 19:43:09 -07:00
holeErrors.lean.expected.out feat: produces an error if the declaration body contains a universe parameter that does not occur in the declaration type nor is explicitly provided 2022-06-02 19:43:09 -07:00
holes.lean
holes.lean.expected.out
hygienicIntro.lean
hygienicIntro.lean.expected.out
implementedByIssue.lean feat: improve implementedBy errors, and relax type matching test 2022-05-02 08:48:15 -07:00
implementedByIssue.lean.expected.out feat: improve implementedBy errors, and relax type matching test 2022-05-02 08:48:15 -07:00
implicitLambdaIssue.lean
implicitLambdaIssue.lean.expected.out
implicitTypePos.lean
implicitTypePos.lean.expected.out
inductionErrors.lean
inductionErrors.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
inductionGen.lean
inductionGen.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
inductionMutual.lean
inductionMutual.lean.expected.out
inductive1.lean
inductive1.lean.expected.out
inductiveUnivErrorMsg.lean feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures 2022-05-10 18:30:53 -07:00
inductiveUnivErrorMsg.lean.expected.out feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures 2022-05-10 18:30:53 -07:00
infoFromFailure.lean
infoFromFailure.lean.expected.out
infoTree.lean
infoTree.lean.expected.out fix: nesting of pattern info nodes 2022-06-27 22:37:02 +02:00
inst.lean
inst.lean.expected.out
intModBug.lean
intModBug.lean.expected.out
intNegSucc.lean
intNegSucc.lean.expected.out
introLetBug.lean fix: intro tactic at let-expr 2022-06-22 16:10:33 -07:00
introLetBug.lean.expected.out fix: intro tactic at let-expr 2022-06-22 16:10:33 -07:00
invalidFieldName.lean
invalidFieldName.lean.expected.out
invalidInstImplicit.lean
invalidInstImplicit.lean.expected.out
invalidNamedArgs.lean
invalidNamedArgs.lean.expected.out
invalidPatternIssue.lean
invalidPatternIssue.lean.expected.out
IRbug.lean
IRbug.lean.expected.out
isDefEqOffsetBug.lean
isDefEqOffsetBug.lean.expected.out
isNoncomputable.lean
isNoncomputable.lean.expected.out
jason1.lean
jason1.lean.expected.out fix: apply after-compilation attributes to inductive/structure decls 2022-05-25 11:32:08 -07:00
jason2.lean
jason2.lean.expected.out
json.lean
json.lean.expected.out
kernelMVarBug.lean
kernelMVarBug.lean.expected.out
keyAttrErase.lean
keyAttrErase.lean.expected.out feat: allow ▸ even if the expected type is not available 2022-04-23 08:00:27 -07:00
lazySeq.lean
lazySeq.lean.expected.out
LE.lean
LE.lean.expected.out
lean3RefineBug.lean
lean3RefineBug.lean.expected.out
letArrowOutsideDo.lean
letArrowOutsideDo.lean.expected.out
letFun.lean
letFun.lean.expected.out
letPatIssue.lean
letPatIssue.lean.expected.out
letrec1.lean
letrec1.lean.expected.out
letrecErrors.lean
letrecErrors.lean.expected.out
letRecMissingAnnotation.lean
letRecMissingAnnotation.lean.expected.out
liftOverLeft.lean
liftOverLeft.lean.expected.out
linterUnusedVariables.lean fix: ignore hygiened names in unused variables linter 2022-06-18 17:24:08 +02:00
linterUnusedVariables.lean.expected.out fix: ignore hygiened names in unused variables linter 2022-06-18 17:24:08 +02:00
listLength.lean
listLength.lean.expected.out
ll_infer_type_bug.lean
ll_infer_type_bug.lean.expected.out
localNotationPP.lean
localNotationPP.lean.expected.out
loopErrorRecovery.lean
loopErrorRecovery.lean.expected.out
lvl1.lean
lvl1.lean.expected.out
macroError.lean
macroError.lean.expected.out
macroPrio.lean
macroPrio.lean.expected.out
macroResolveName.lean refactor: resolveNamespace now return a List 2022-06-16 17:16:36 -07:00
macroResolveName.lean.expected.out refactor: resolveNamespace now return a List 2022-06-16 17:16:36 -07:00
macroscopes.lean
macroscopes.lean.expected.out
macroStack.lean
macroStack.lean.expected.out feat: improve binrel% elaborator 2022-05-09 18:39:52 -07:00
macroTrace.lean
macroTrace.lean.expected.out
magical.lean
magical.lean.expected.out
mangling.lean
mangling.lean.expected.out
match1.lean
match1.lean.expected.out
match2.lean
match2.lean.expected.out
match3.lean
match3.lean.expected.out
match4.lean
match4.lean.expected.out
matchAltIndent.lean
matchAltIndent.lean.expected.out
matchApp.lean
matchApp.lean.expected.out
matchErrorLocation.lean
matchErrorLocation.lean.expected.out
matchErrorMsg.lean
matchErrorMsg.lean.expected.out fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
matchLeftovers.lean
matchLeftovers.lean.expected.out
matchMissingCasesAsStuckError.lean
matchMissingCasesAsStuckError.lean.expected.out fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
matchMultAlt.lean
matchMultAlt.lean.expected.out
matchOfNatIssue.lean
matchOfNatIssue.lean.expected.out
matchOrIssue.lean fix: match or-pattern 2022-05-25 20:05:46 -07:00
matchOrIssue.lean.expected.out fix: match or-pattern 2022-05-25 20:05:46 -07:00
matchPatternInsideBinders.lean
matchPatternInsideBinders.lean.expected.out fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
matchPatternPartialApp.lean
matchPatternPartialApp.lean.expected.out fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
matchunit.lean
matchunit.lean.expected.out
matchUnknownFVarBug.lean
matchUnknownFVarBug.lean.expected.out fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
matchVarNames.lean
matchVarNames.lean.expected.out
metaEvalInstMessage.lean
metaEvalInstMessage.lean.expected.out
missingExplicitWithForwardNamedDep.lean
missingExplicitWithForwardNamedDep.lean.expected.out
mkProjStx.lean
mkProjStx.lean.expected.out
modBug.lean
modBug.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
moduleDoc.lean
moduleDoc.lean.expected.out
moduleOf.lean
moduleOf.lean.expected.out
mulcommErrorMessage.lean
mulcommErrorMessage.lean.expected.out chore: normalize spelling 2022-05-03 10:26:11 +02:00
multiConstantError.lean chore: fix tests 2022-06-14 16:43:22 -07:00
multiConstantError.lean.expected.out chore: fix tests 2022-06-14 17:27:13 -07:00
mutualdef1.lean
mutualdef1.lean.expected.out
mutualWithNamespaceMacro.lean
mutualWithNamespaceMacro.lean.expected.out
mutwf1.lean
mutwf1.lean.expected.out
mvar1.lean
mvar1.lean.expected.out
mvar2.lean
mvar2.lean.expected.out
mvar3.lean
mvar3.lean.expected.out
mvar_fvar.lean
mvar_fvar.lean.expected.out
mvarAtDefaultValue.lean
mvarAtDefaultValue.lean.expected.out
nameArgErrorIssue.lean feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
nameArgErrorIssue.lean.expected.out chore: fix tests 2022-05-31 18:17:56 -07:00
namedHoles.lean
namedHoles.lean.expected.out chore: fix tests 2022-05-31 18:17:56 -07:00
namelit.lean
namelit.lean.expected.out
namePatEqThm.lean
namePatEqThm.lean.expected.out
nameRepr.lean
nameRepr.lean.expected.out
negFloat.lean
negFloat.lean.expected.out
newCatPanic.lean
newCatPanic.lean.expected.out
nonAtomicFieldName.lean
nonAtomicFieldName.lean.expected.out
noncompSection.lean
noncompSection.lean.expected.out
nondepArrow.lean
nondepArrow.lean.expected.out
nonReserved.lean
nonReserved.lean.expected.out
noTabs.lean
noTabs.lean.expected.out
notationDelab.lean feat: improve the heuristic for notation delab 2022-06-23 13:27:53 -07:00
notationDelab.lean.expected.out feat: improve the heuristic for notation delab 2022-06-23 13:27:53 -07:00
notationPrecheck.lean
notationPrecheck.lean.expected.out
openExport.lean
openExport.lean.expected.out
openScoped.lean
openScoped.lean.expected.out
or_shortcircuit.lean
or_shortcircuit.lean.expected.out
parserPrio.lean
parserPrio.lean.expected.out
partialVariable.lean
partialVariable.lean.expected.out
patvar.lean
patvar.lean.expected.out fix: no sorry-warning for missing match cases 2022-06-01 07:41:52 -07:00
phashmap_inst_coherence.lean
phashmap_inst_coherence.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
ppExpr.lean
ppExpr.lean.expected.out
PPInstances.lean chore: fix tests 2022-06-14 16:43:22 -07:00
PPInstances.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
ppite.lean
ppite.lean.expected.out
pplevel.lean
pplevel.lean.expected.out
ppMotives.lean
ppMotives.lean.expected.out
ppNotationCode.lean
ppNotationCode.lean.expected.out
ppProofs.lean
ppProofs.lean.expected.out
PPRoundtrip.lean fix: test 2022-06-17 17:47:51 -07:00
PPRoundtrip.lean.expected.out
ppSyntax.lean
ppSyntax.lean.expected.out
precissues.lean
precissues.lean.expected.out
private.lean
private.lean.expected.out
privateFieldCopyIssue.lean
privateFieldCopyIssue.lean.expected.out
Process.lean
Process.lean.expected.out
protected.lean
protected.lean.expected.out
pureCoeIssue.lean
pureCoeIssue.lean.expected.out
rat1.lean
rat1.lean.expected.out
readDir.lean
readDir.lean.expected.out
redundantAlt.lean
redundantAlt.lean.expected.out
ref1.lean
ref1.lean.expected.out
refineOccursCheck.lean
refineOccursCheck.lean.expected.out
Reformat.lean feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
Reformat.lean.expected.out chore: fix tests 2022-06-14 17:27:13 -07:00
renameBug.lean
renameBug.lean.expected.out
renameI.lean
renameI.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
repr.lean
repr.lean.expected.out
repr_issue.lean
repr_issue.lean.expected.out
resolveGlobalName.lean feat: implement MonadLog at CoreM 2022-05-31 17:40:55 -07:00
resolveGlobalName.lean.expected.out
revertlet.lean
revertlet.lean.expected.out
rewrite.lean
rewrite.lean.expected.out
rfl_simp_thm.lean feat: track rfl simp theorems 2022-04-21 13:42:04 -07:00
rfl_simp_thm.lean.expected.out feat: track rfl simp theorems 2022-04-21 13:42:04 -07:00
root.lean chore: fix test 2022-06-13 14:06:56 -07:00
root.lean.expected.out chore: fix test 2022-06-13 14:06:56 -07:00
runSTBug.lean
runSTBug.lean.expected.out
rwEqThms.lean
rwEqThms.lean.expected.out chore: fix test 2022-06-07 16:37:45 -07:00
rwWithoutOffsetCnstrs.lean
rwWithoutOffsetCnstrs.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
safeShadowing.lean
safeShadowing.lean.expected.out
sanitizeMacroScopes.lean
sanitizeMacroScopes.lean.expected.out
sanitychecks.lean chore: fix tests 2022-06-14 16:43:22 -07:00
sanitychecks.lean.expected.out chore: fix tests 2022-06-14 17:27:13 -07:00
scopedInstanceOutsideNamespace.lean
scopedInstanceOutsideNamespace.lean.expected.out
scopedLocalInsts.lean
scopedLocalInsts.lean.expected.out
scopedMacros.lean
scopedMacros.lean.expected.out
scopedTokens.lean
scopedTokens.lean.expected.out
scopedunifhint.lean
scopedunifhint.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
semicolonOrLinebreak.lean fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate 2022-06-16 23:33:57 +02:00
semicolonOrLinebreak.lean.expected.out fix: introduce semicolonOrLinebreak, replace many(1) with sepBy(1) where appropriate 2022-06-16 23:33:57 +02:00
sepByIndentQuot.lean chore: add test for sepByIndent.formatter 2022-06-24 10:59:55 +02:00
sepByIndentQuot.lean.expected.out chore: add test for sepByIndent.formatter 2022-06-24 10:59:55 +02:00
shadow.lean
shadow.lean.expected.out
simpArgTypeMismatch.lean
simpArgTypeMismatch.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
simpcfg.lean
simpcfg.lean.expected.out
simpDisch.lean chore: fix tests 2022-06-14 16:43:22 -07:00
simpDisch.lean.expected.out
simpPrefixIssue.lean
simpPrefixIssue.lean.expected.out
simpZetaFalse.lean chore: fix tests 2022-06-14 16:43:22 -07:00
simpZetaFalse.lean.expected.out chore: unused variables 2022-06-07 17:54:10 -07:00
sizeof.lean
sizeof.lean.expected.out
smartUnfolding.lean
smartUnfolding.lean.expected.out
smartUnfoldingMatch.lean chore: fix tests 2022-06-14 16:43:22 -07:00
smartUnfoldingMatch.lean.expected.out
sorryAtError.lean
sorryAtError.lean.expected.out feat: improve argument type mismatch error position, and do not stop at application type mismatch errors 2022-04-25 16:30:40 -07:00
sorryWarning.lean
sorryWarning.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
splitIssue.lean
splitIssue.lean.expected.out
stdio.lean
stdio.lean.expected.out
stream.lean
stream.lean.expected.out
strictImplicit.lean
strictImplicit.lean.expected.out
string_imp.lean
string_imp.lean.expected.out
string_imp2.lean
string_imp2.lean.expected.out
struct1.lean
struct1.lean.expected.out
structAutoBound.lean
structAutoBound.lean.expected.out
structDefault.lean
structDefault.lean.expected.out
structDefValueOverride.lean
structDefValueOverride.lean.expected.out
structInst1.lean
structInst1.lean.expected.out
structInstError.lean
structInstError.lean.expected.out
structSorryBug.lean
structSorryBug.lean.expected.out
structuralEqns.lean
structuralEqns.lean.expected.out
StxQuot.lean feat: $_ antiquotation pattern 2022-06-04 13:57:04 +02:00
StxQuot.lean.expected.out chore: fix tests 2022-06-16 23:33:57 +02:00
substBadMotive.lean
substBadMotive.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
substlet.lean
substlet.lean.expected.out
syntaxErrors.lean
syntaxErrors.lean.expected.out
syntaxInNamespacesAndPP.lean
syntaxInNamespacesAndPP.lean.expected.out
syntaxPrec.lean
syntaxPrec.lean.expected.out
syntheticHolesAsPatterns.lean
syntheticHolesAsPatterns.lean.expected.out
tabulate.lean
tabulate.lean.expected.out
tacUnsolvedGoalsErrors.lean
tacUnsolvedGoalsErrors.lean.expected.out
tcloop.lean
tcloop.lean.expected.out
termination_by.lean
termination_by.lean.expected.out
termination_by2.lean
termination_by2.lean.expected.out
terminationFailure.lean
terminationFailure.lean.expected.out
test_single.sh fix: unused variables linter review comments 2022-06-03 13:03:52 +02:00
theoremType.lean
theoremType.lean.expected.out
thunk.lean
thunk.lean.expected.out
toFieldNameIssue.lean
toFieldNameIssue.lean.expected.out
tokenErrors.lean
tokenErrors.lean.expected.out
tooManyVarsAtInduction.lean
tooManyVarsAtInduction.lean.expected.out chore: fix tests 2022-06-01 06:36:25 -07:00
traceClassScopes.lean
traceClassScopes.lean.expected.out
traceStateBactracking.lean
traceStateBactracking.lean.expected.out
traceTacticSteps.lean
traceTacticSteps.lean.expected.out feat: annotate <;> with expected state 2022-04-29 16:16:09 +02:00
treeMap.lean
treeMap.lean.expected.out
typeIncorrectPat.lean
typeIncorrectPat.lean.expected.out
typeMismatch.lean
typeMismatch.lean.expected.out
typeOf.lean
typeOf.lean.expected.out
uintCtors.lean
uintCtors.lean.expected.out
uintMatch.lean
uintMatch.lean.expected.out
unboxStruct.lean chore: fix tests 2022-06-14 16:43:22 -07:00
unboxStruct.lean.expected.out
unexpander.lean
unexpander.lean.expected.out
unexpandersNamespaces.lean
unexpandersNamespaces.lean.expected.out
UnexpandSubtype.lean
UnexpandSubtype.lean.expected.out
unfold1.lean fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one 2022-06-06 15:53:40 -07:00
unfold1.lean.expected.out fix: unfold declarations tagged with [matchPattern] at reduceMatcher? even if transparency setting is not the default one 2022-06-06 15:53:40 -07:00
unfoldDefEq.lean
unfoldDefEq.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
unfoldFailure.lean feat: unfold should fail if it didn't unfold anything 2022-05-09 06:41:17 -07:00
unfoldFailure.lean.expected.out feat: unfold should fail if it didn't unfold anything 2022-05-09 06:41:17 -07:00
unfoldReduceMatch.lean feat: unfold tactic tries to reduce match after unfolding 2022-05-09 06:35:40 -07:00
unfoldReduceMatch.lean.expected.out chore: fix tests 2022-05-31 18:01:48 -07:00
unhygienic.lean
unhygienic.lean.expected.out
unifHintAndTC.lean
unifHintAndTC.lean.expected.out
univInference.lean
univInference.lean.expected.out feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures 2022-05-10 18:30:53 -07:00
unknownId.lean
unknownId.lean.expected.out
unknownTactic.lean
unknownTactic.lean.expected.out
unnecessaryUnfolding.lean
unnecessaryUnfolding.lean.expected.out
unsolvedIndCases.lean
unsolvedIndCases.lean.expected.out
unsound.lean
unsound.lean.expected.out
unused_univ.lean
unused_univ.lean.expected.out
unusedLet.lean
unusedLet.lean.expected.out
wf1.lean
wf1.lean.expected.out
wf2.lean
wf2.lean.expected.out
wfrecUnusedLet.lean
wfrecUnusedLet.lean.expected.out chore: unused variables 2022-06-07 17:54:10 -07:00
whnfProj.lean
whnfProj.lean.expected.out
wildcardAlt.lean
wildcardAlt.lean.expected.out
zipper.lean
zipper.lean.expected.out