Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-04 00:48
97add9b7
View on Github →
chore: make tests into a library (
#18304
)
Estimated changes
Renamed
test/AdmitLinter.lean
to
MathlibTest/AdmitLinter.lean
Renamed
test/ApplyAt.lean
to
MathlibTest/ApplyAt.lean
Renamed
test/ArithMult.lean
to
MathlibTest/ArithMult.lean
Renamed
test/AssertExists.lean
to
MathlibTest/AssertExists.lean
Renamed
test/AssertImported.lean
to
MathlibTest/AssertImported.lean
Renamed
test/BinPow.lean
to
MathlibTest/BinPow.lean
Renamed
test/BinaryRec.lean
to
MathlibTest/BinaryRec.lean
Renamed
test/Bound/attribute.lean
to
MathlibTest/Bound/attribute.lean
Renamed
test/Bound/bound.lean
to
MathlibTest/Bound/bound.lean
Renamed
test/CategoryTheory/Bicategory/Basic.lean
to
MathlibTest/CategoryTheory/Bicategory/Basic.lean
Renamed
test/CategoryTheory/Bicategory/Normalize.lean
to
MathlibTest/CategoryTheory/Bicategory/Normalize.lean
Renamed
test/CategoryTheory/Coherence.lean
to
MathlibTest/CategoryTheory/Coherence.lean
Renamed
test/CategoryTheory/Elementwise.lean
to
MathlibTest/CategoryTheory/Elementwise.lean
Renamed
test/CategoryTheory/Mon_.lean
to
MathlibTest/CategoryTheory/Mon_.lean
Renamed
test/CategoryTheory/Monoidal/Basic.lean
to
MathlibTest/CategoryTheory/Monoidal/Basic.lean
Renamed
test/CategoryTheory/Monoidal/Normalize.lean
to
MathlibTest/CategoryTheory/Monoidal/Normalize.lean
Renamed
test/CategoryTheory/MonoidalComp.lean
to
MathlibTest/CategoryTheory/MonoidalComp.lean
Renamed
test/CategoryTheory/PrettyPrinting.lean
to
MathlibTest/CategoryTheory/PrettyPrinting.lean
Renamed
test/CategoryTheory/Sites/ConcreteSheafification.lean
to
MathlibTest/CategoryTheory/Sites/ConcreteSheafification.lean
Renamed
test/CategoryTheory/Sites/PreservesSheafification.lean
to
MathlibTest/CategoryTheory/Sites/PreservesSheafification.lean
Renamed
test/CategoryTheory/Sites/Whiskering.lean
to
MathlibTest/CategoryTheory/Sites/Whiskering.lean
Renamed
test/CategoryTheory/Slice.lean
to
MathlibTest/CategoryTheory/Slice.lean
Renamed
test/CategoryTheory/SubstHomLift.lean
to
MathlibTest/CategoryTheory/SubstHomLift.lean
Renamed
test/CategoryTheory/ToApp.lean
to
MathlibTest/CategoryTheory/ToApp.lean
Renamed
test/Change.lean
to
MathlibTest/Change.lean
Renamed
test/Check.lean
to
MathlibTest/Check.lean
Renamed
test/Clean.lean
to
MathlibTest/Clean.lean
Renamed
test/Clear!.lean
to
MathlibTest/Clear!.lean
Renamed
test/ClearExcept.lean
to
MathlibTest/ClearExcept.lean
Renamed
test/ClearValue.lean
to
MathlibTest/ClearValue.lean
Renamed
test/Clear_.lean
to
MathlibTest/Clear_.lean
Renamed
test/CommDiag.lean
to
MathlibTest/CommDiag.lean
Renamed
test/CompileInductive.lean
to
MathlibTest/CompileInductive.lean
Renamed
test/Complex.lean
to
MathlibTest/Complex.lean
Renamed
test/ComputeDegree.lean
to
MathlibTest/ComputeDegree.lean
Renamed
test/Constructor.lean
to
MathlibTest/Constructor.lean
Renamed
test/Continuity.lean
to
MathlibTest/Continuity.lean
Renamed
test/Contrapose.lean
to
MathlibTest/Contrapose.lean
Renamed
test/CountHeartbeats.lean
to
MathlibTest/CountHeartbeats.lean
Renamed
test/DFinsuppMultiLinear.lean
to
MathlibTest/DFinsuppMultiLinear.lean
Renamed
test/DefEqTransformations.lean
to
MathlibTest/DefEqTransformations.lean
Renamed
test/DeprecateMe.lean
to
MathlibTest/DeprecateMe.lean
Renamed
test/DeriveFintype.lean
to
MathlibTest/DeriveFintype.lean
Renamed
test/DeriveToExpr.lean
to
MathlibTest/DeriveToExpr.lean
added
inductive
DeriveToExprTests.A
added
inductive
DeriveToExprTests.B
added
inductive
DeriveToExprTests.Bar
added
inductive
DeriveToExprTests.C
added
inductive
DeriveToExprTests.D
added
inductive
DeriveToExprTests.Foo
added
inductive
DeriveToExprTests.MyMaybe
added
def
DeriveToExprTests.boolFunHelper
deleted
inductive
tests.A
deleted
inductive
tests.B
deleted
inductive
tests.Bar
deleted
inductive
tests.C
deleted
inductive
tests.D
deleted
inductive
tests.Foo
deleted
inductive
tests.MyMaybe
deleted
def
tests.boolFunHelper
Renamed
test/DocPrime.lean
to
MathlibTest/DocPrime.lean
Renamed
test/DualNumber.lean
to
MathlibTest/DualNumber.lean
Renamed
test/ExistsI.lean
to
MathlibTest/ExistsI.lean
Renamed
test/Explode.lean
to
MathlibTest/Explode.lean
Renamed
test/Expr.lean
to
MathlibTest/Expr.lean
Renamed
test/ExtractGoal.lean
to
MathlibTest/ExtractGoal.lean
Renamed
test/ExtractLets.lean
to
MathlibTest/ExtractLets.lean
Renamed
test/FBinop.lean
to
MathlibTest/FBinop.lean
Renamed
test/FieldSimp.lean
to
MathlibTest/FieldSimp.lean
Renamed
test/Find.lean
to
MathlibTest/Find.lean
Renamed
test/FlexibleLinter.lean
to
MathlibTest/FlexibleLinter.lean
Renamed
test/FunLike.lean
to
MathlibTest/FunLike.lean
Renamed
test/GCongr/inequalities.lean
to
MathlibTest/GCongr/inequalities.lean
added
def
GCongrTests.dontUnfoldMe
deleted
def
dontUnfoldMe
Renamed
test/GCongr/mod.lean
to
MathlibTest/GCongr/mod.lean
Renamed
test/GeneralizeProofs.lean
to
MathlibTest/GeneralizeProofs.lean
Renamed
test/Group.lean
to
MathlibTest/Group.lean
Renamed
test/GuardGoalNums.lean
to
MathlibTest/GuardGoalNums.lean
Renamed
test/GuardHypNums.lean
to
MathlibTest/GuardHypNums.lean
Renamed
test/HashCommandLinter.lean
to
MathlibTest/HashCommandLinter.lean
Renamed
test/Have.lean
to
MathlibTest/Have.lean
Renamed
test/HaveLetLinter.lean
to
MathlibTest/HaveLetLinter.lean
Renamed
test/Header.lean
to
MathlibTest/Header.lean
Renamed
test/HigherOrder.lean
to
MathlibTest/HigherOrder.lean
Renamed
test/ImplicitUniverses.lean
to
MathlibTest/ImplicitUniverses.lean
Renamed
test/InferParam.lean
to
MathlibTest/InferParam.lean
Renamed
test/Inhabit.lean
to
MathlibTest/Inhabit.lean
added
structure
InhabitTests.Unique
deleted
structure
Unique
Renamed
test/InstanceTransparency.lean
to
MathlibTest/InstanceTransparency.lean
Renamed
test/IsBoundedDefault.lean
to
MathlibTest/IsBoundedDefault.lean
Renamed
test/LibrarySearch/IsCompact.lean
to
MathlibTest/LibrarySearch/IsCompact.lean
Renamed
test/LibrarySearch/basic.lean
to
MathlibTest/LibrarySearch/basic.lean
Renamed
test/LibrarySearch/mathlib.lean
to
MathlibTest/LibrarySearch/mathlib.lean
Renamed
test/LibrarySearch/observe.lean
to
MathlibTest/LibrarySearch/observe.lean
Renamed
test/LiftLets.lean
to
MathlibTest/LiftLets.lean
Renamed
test/Lint.lean
to
MathlibTest/Lint.lean
Renamed
test/LintStyle.lean
to
MathlibTest/LintStyle.lean
Renamed
test/LongFile.lean
to
MathlibTest/LongFile.lean
Renamed
test/MaxPowDiv.lean
to
MathlibTest/MaxPowDiv.lean
Renamed
test/MfldSetTac.lean
to
MathlibTest/MfldSetTac.lean
Renamed
test/MinImports.lean
to
MathlibTest/MinImports.lean
Renamed
test/MkIffOfInductive.lean
to
MathlibTest/MkIffOfInductive.lean
Renamed
test/MonCat.lean
to
MathlibTest/MonCat.lean
Renamed
test/Monotonicity.lean
to
MathlibTest/Monotonicity.lean
Renamed
test/MoveAdd.lean
to
MathlibTest/MoveAdd.lean
Renamed
test/Multigoal.lean
to
MathlibTest/Multigoal.lean
Renamed
test/NoncommRing.lean
to
MathlibTest/NoncommRing.lean
Renamed
test/NthRewrite.lean
to
MathlibTest/NthRewrite.lean
Renamed
test/PPRoundtrip.lean
to
MathlibTest/PPRoundtrip.lean
Renamed
test/Polynomial.lean
to
MathlibTest/Polynomial.lean
Renamed
test/PosDef.lean
to
MathlibTest/PosDef.lean
Renamed
test/ProdAssoc.lean
to
MathlibTest/ProdAssoc.lean
Renamed
test/Qify.lean
to
MathlibTest/Qify.lean
Renamed
test/Quaternion.lean
to
MathlibTest/Quaternion.lean
Renamed
test/Real.lean
to
MathlibTest/Real.lean
Renamed
test/Recall.lean
to
MathlibTest/Recall.lean
Renamed
test/RefineLinter.lean
to
MathlibTest/RefineLinter.lean
Renamed
test/RegularMeasure.lean
to
MathlibTest/RegularMeasure.lean
Renamed
test/Rename.lean
to
MathlibTest/Rename.lean
Renamed
test/Replace.lean
to
MathlibTest/Replace.lean
Renamed
test/RewriteSearch/Basic.lean
to
MathlibTest/RewriteSearch/Basic.lean
Renamed
test/RewriteSearch/Polynomial.lean
to
MathlibTest/RewriteSearch/Polynomial.lean
Renamed
test/Rify.lean
to
MathlibTest/Rify.lean
Renamed
test/Set.lean
to
MathlibTest/Set.lean
Renamed
test/Simp.lean
to
MathlibTest/Simp.lean
Renamed
test/SimpRw.lean
to
MathlibTest/SimpRw.lean
Renamed
test/Simps.lean
to
MathlibTest/Simps.lean
Renamed
test/Split.lean
to
MathlibTest/Split.lean
Renamed
test/SplitIfs.lean
to
MathlibTest/SplitIfs.lean
Renamed
test/StacksAttribute.lean
to
MathlibTest/StacksAttribute.lean
Renamed
test/StringDiagram.lean
to
MathlibTest/StringDiagram.lean
Renamed
test/Subsingleton.lean
to
MathlibTest/Subsingleton.lean
Renamed
test/SwapVar.lean
to
MathlibTest/SwapVar.lean
Renamed
test/TCSynth.lean
to
MathlibTest/TCSynth.lean
Renamed
test/Tauto.lean
to
MathlibTest/Tauto.lean
Renamed
test/TermBeta.lean
to
MathlibTest/TermBeta.lean
Renamed
test/TermCongr.lean
to
MathlibTest/TermCongr.lean
Renamed
test/TermCongr2.lean
to
MathlibTest/TermCongr2.lean
Renamed
test/Traversable.lean
to
MathlibTest/Traversable.lean
Renamed
test/TypeCheck.lean
to
MathlibTest/TypeCheck.lean
Renamed
test/UnsetOption.lean
to
MathlibTest/UnsetOption.lean
Renamed
test/UnusedTactic.lean
to
MathlibTest/UnusedTactic.lean
Renamed
test/Use.lean
to
MathlibTest/Use.lean
Renamed
test/ValuedCSP.lean
to
MathlibTest/ValuedCSP.lean
Renamed
test/Variable.lean
to
MathlibTest/Variable.lean
Renamed
test/Zify.lean
to
MathlibTest/Zify.lean
Renamed
test/abel.lean
to
MathlibTest/abel.lean
Renamed
test/aesop_cat.lean
to
MathlibTest/aesop_cat.lean
Renamed
test/algebraize.lean
to
MathlibTest/algebraize.lean
Renamed
test/antidiagonal.lean
to
MathlibTest/antidiagonal.lean
Renamed
test/apply_congr.lean
to
MathlibTest/apply_congr.lean
Renamed
test/apply_fun.lean
to
MathlibTest/apply_fun.lean
Renamed
test/apply_rules.lean
to
MathlibTest/apply_rules.lean
Renamed
test/apply_with.lean
to
MathlibTest/apply_with.lean
Renamed
test/basicTactics.lean
to
MathlibTest/basicTactics.lean
Renamed
test/borelize.lean
to
MathlibTest/borelize.lean
Renamed
test/byContra.lean
to
MathlibTest/byContra.lean
Renamed
test/cancel_denoms.lean
to
MathlibTest/cancel_denoms.lean
Renamed
test/cases.lean
to
MathlibTest/cases.lean
Renamed
test/casesm.lean
to
MathlibTest/casesm.lean
Renamed
test/cc.lean
to
MathlibTest/cc.lean
Renamed
test/choose.lean
to
MathlibTest/choose.lean
Renamed
test/choose_reduction.lean
to
MathlibTest/choose_reduction.lean
Renamed
test/coe.lean
to
MathlibTest/coe.lean
Renamed
test/congr.lean
to
MathlibTest/congr.lean
Renamed
test/congrm.lean
to
MathlibTest/congrm.lean
Renamed
test/conv.lean
to
MathlibTest/conv.lean
Renamed
test/convert.lean
to
MathlibTest/convert.lean
Renamed
test/convert2.lean
to
MathlibTest/convert2.lean
Renamed
test/delabLinearIndependent.lean
to
MathlibTest/delabLinearIndependent.lean
Renamed
test/delaborators.lean
to
MathlibTest/delaborators.lean
Renamed
test/dfinsupp_notation.lean
to
MathlibTest/dfinsupp_notation.lean
Renamed
test/eqns.lean
to
MathlibTest/eqns.lean
Renamed
test/eval_elab.lean
to
MathlibTest/eval_elab.lean
Renamed
test/fail_if_no_progress.lean
to
MathlibTest/fail_if_no_progress.lean
Renamed
test/fin_cases.lean
to
MathlibTest/fin_cases.lean
Renamed
test/finiteness.lean
to
MathlibTest/finiteness.lean
Renamed
test/finset_builder.lean
to
MathlibTest/finset_builder.lean
Renamed
test/finset_repr.lean
to
MathlibTest/finset_repr.lean
Renamed
test/finsupp_notation.lean
to
MathlibTest/finsupp_notation.lean
Renamed
test/format_table.lean
to
MathlibTest/format_table.lean
Renamed
test/fun_prop.lean
to
MathlibTest/fun_prop.lean
Renamed
test/fun_prop2.lean
to
MathlibTest/fun_prop2.lean
Renamed
test/fun_prop_dev.lean
to
MathlibTest/fun_prop_dev.lean
Renamed
test/globalAttributeIn.lean
to
MathlibTest/globalAttributeIn.lean
Renamed
test/hint.lean
to
MathlibTest/hint.lean
Renamed
test/import_all.lean
to
MathlibTest/import_all.lean
Renamed
test/instance_diamonds.lean
to
MathlibTest/instance_diamonds.lean
Renamed
test/instance_diamonds/Data/Complex/Module.lean
to
MathlibTest/instance_diamonds/Data/Complex/Module.lean
Renamed
test/instance_diamonds/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
to
MathlibTest/instance_diamonds/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
Renamed
test/instance_diamonds/FieldTheory/SplittingField/Construction.lean
to
MathlibTest/instance_diamonds/FieldTheory/SplittingField/Construction.lean
Renamed
test/instance_diamonds/algebra_rat.lean
to
MathlibTest/instance_diamonds/algebra_rat.lean
Renamed
test/instance_diamonds/normed.lean
to
MathlibTest/instance_diamonds/normed.lean
Renamed
test/instances/CommRing_integralClosure.lean
to
MathlibTest/instances/CommRing_integralClosure.lean
Renamed
test/instances/Ring_finiteness.lean
to
MathlibTest/instances/Ring_finiteness.lean
Renamed
test/interactiveUnfold.lean
to
MathlibTest/interactiveUnfold.lean
Renamed
test/interval_cases.lean
to
MathlibTest/interval_cases.lean
Renamed
test/irreducibleDef.lean
to
MathlibTest/irreducibleDef.lean
Renamed
test/itauto.lean
to
MathlibTest/itauto.lean
Renamed
test/jacobiSym.lean
to
MathlibTest/jacobiSym.lean
Renamed
test/levenshtein.lean
to
MathlibTest/levenshtein.lean
Renamed
test/lift.lean
to
MathlibTest/lift.lean
Renamed
test/linarith.lean
to
MathlibTest/linarith.lean
Renamed
test/linear_combination'.lean
to
MathlibTest/linear_combination'.lean
Renamed
test/linear_combination.lean
to
MathlibTest/linear_combination.lean
Renamed
test/matrix.lean
to
MathlibTest/matrix.lean
Renamed
test/measurability.lean
to
MathlibTest/measurability.lean
Renamed
test/meta.lean
to
MathlibTest/meta.lean
Renamed
test/mod_cases.lean
to
MathlibTest/mod_cases.lean
Renamed
test/module.lean
to
MathlibTest/module.lean
Renamed
test/nomatch.lean
to
MathlibTest/nomatch.lean
Renamed
test/nontriviality.lean
to
MathlibTest/nontriviality.lean
Renamed
test/norm_cast.lean
to
MathlibTest/norm_cast.lean
Renamed
test/norm_num.lean
to
MathlibTest/norm_num.lean
Renamed
test/norm_num_ext.lean
to
MathlibTest/norm_num_ext.lean
Renamed
test/norm_num_rpow.lean
to
MathlibTest/norm_num_rpow.lean
Renamed
test/notation3.lean
to
MathlibTest/notation3.lean
Renamed
test/observe.lean
to
MathlibTest/observe.lean
Renamed
test/oldObtain.lean
to
MathlibTest/oldObtain.lean
Renamed
test/peel.lean
to
MathlibTest/peel.lean
Renamed
test/polyrith.lean
to
MathlibTest/polyrith.lean
Renamed
test/positivity.lean
to
MathlibTest/positivity.lean
Renamed
test/propose.lean
to
MathlibTest/propose.lean
Renamed
test/push_neg.lean
to
MathlibTest/push_neg.lean
Renamed
test/random.lean
to
MathlibTest/random.lean
Renamed
test/recover.lean
to
MathlibTest/recover.lean
Renamed
test/reduce_mod_char.lean
to
MathlibTest/reduce_mod_char.lean
Renamed
test/renameBvar.lean
to
MathlibTest/renameBvar.lean
Renamed
test/rewrites.lean
to
MathlibTest/rewrites.lean
Renamed
test/right_actions.lean
to
MathlibTest/right_actions.lean
Renamed
test/ring.lean
to
MathlibTest/ring.lean
Renamed
test/ring_compare.lean
to
MathlibTest/ring_compare.lean
Renamed
test/rsuffices.lean
to
MathlibTest/rsuffices.lean
Renamed
test/runCmd.lean
to
MathlibTest/runCmd.lean
Renamed
test/says.lean
to
MathlibTest/says.lean
Renamed
test/search/BestFirst.lean
to
MathlibTest/search/BestFirst.lean
Renamed
test/set_like.lean
to
MathlibTest/set_like.lean
Renamed
test/simp_confluence.lean
to
MathlibTest/simp_confluence.lean
Renamed
test/simp_intro.lean
to
MathlibTest/simp_intro.lean
Renamed
test/slim_check.lean
to
MathlibTest/slim_check.lean
Renamed
test/slow_simp.lean
to
MathlibTest/slow_simp.lean
Renamed
test/solve_by_elim/basic.lean
to
MathlibTest/solve_by_elim/basic.lean
Renamed
test/solve_by_elim/instances.lean
to
MathlibTest/solve_by_elim/instances.lean
Renamed
test/spread.lean
to
MathlibTest/spread.lean
Renamed
test/success_if_fail_with_msg.lean
to
MathlibTest/success_if_fail_with_msg.lean
Renamed
test/superscript.lean
to
MathlibTest/superscript.lean
Renamed
test/symm.lean
to
MathlibTest/symm.lean
Renamed
test/tactic_timeout.lean
to
MathlibTest/tactic_timeout.lean
Renamed
test/tfae.lean
to
MathlibTest/tfae.lean
Renamed
test/toAdditive.lean
to
MathlibTest/toAdditive.lean
Renamed
test/toAdditiveIrredDef.lean
to
MathlibTest/toAdditiveIrredDef.lean
Renamed
test/trace.lean
to
MathlibTest/trace.lean
Renamed
test/vec_notation.lean
to
MathlibTest/vec_notation.lean
Renamed
test/wlog.lean
to
MathlibTest/wlog.lean
Renamed
test/zmod.lean
to
MathlibTest/zmod.lean
Modified
lakefile.lean
Modified
scripts/mk_all.lean