mathlib4/MathlibTest at master · manman4/mathlib4

History

Name		Name	Last commit message	Last commit date
parent directory ..
Algebra		Algebra
Bound		Bound
CategoryTheory		CategoryTheory
Delab		Delab
DifferentialGeometry		DifferentialGeometry
DirectoryDependencyLinter		DirectoryDependencyLinter
GCongr		GCongr
LibrarySearch		LibrarySearch
LibrarySuggestions		LibrarySuggestions
Nat		Nat
PrivateModuleLinter		PrivateModuleLinter
Simproc		Simproc
UnusedInstancesInType		UnusedInstancesInType
Util		Util
grind		grind
instance_diamonds		instance_diamonds
instances		instances
search		search
solve_by_elim		solve_by_elim
AesopUnusedTactic.lean		AesopUnusedTactic.lean
ApplyAt.lean		ApplyAt.lean
ArithMult.lean		ArithMult.lean
AssertExists.lean		AssertExists.lean
AssertImported.lean		AssertImported.lean
BigOps.lean		BigOps.lean
BinPow.lean		BinPow.lean
BinaryRec.lean		BinaryRec.lean
CalcQuestionMark.lean		CalcQuestionMark.lean
Change.lean		Change.lean
Check.lean		Check.lean
Clean.lean		Clean.lean
ClearExcept.lean		ClearExcept.lean
ClearExclamation.lean		ClearExclamation.lean
ClearValue.lean		ClearValue.lean
Clear_.lean		Clear_.lean
CommDiag.lean		CommDiag.lean
CompileInductive.lean		CompileInductive.lean
Complex.lean		Complex.lean
ComputeDegree.lean		ComputeDegree.lean
Constructor.lean		Constructor.lean
Continuity.lean		Continuity.lean
Contrapose.lean		Contrapose.lean
CountHeartbeats.lean		CountHeartbeats.lean
DFinsuppMultiLinear.lean		DFinsuppMultiLinear.lean
DefEqTransformations.lean		DefEqTransformations.lean
DeprecateTo.lean		DeprecateTo.lean
DeprecatedModule.lean		DeprecatedModule.lean
DeprecatedModuleAllTest.lean		DeprecatedModuleAllTest.lean
DeprecatedModuleMetaTest.lean		DeprecatedModuleMetaTest.lean
DeprecatedModuleNew.lean		DeprecatedModuleNew.lean
DeprecatedModulePublicMetaTest.lean		DeprecatedModulePublicMetaTest.lean
DeprecatedModulePublicTest.lean		DeprecatedModulePublicTest.lean
DeprecatedModuleTest.lean		DeprecatedModuleTest.lean
DeprecatedSyntaxLinter.lean		DeprecatedSyntaxLinter.lean
Deriv.lean		Deriv.lean
DeriveFintype.lean		DeriveFintype.lean
DeriveToExpr.lean		DeriveToExpr.lean
DocPrime.lean		DocPrime.lean
DocString.lean		DocString.lean
DoubleUnderscore.lean		DoubleUnderscore.lean
DualNumber.lean		DualNumber.lean
EmptyLine.lean		EmptyLine.lean
Equiv.lean		Equiv.lean
ErwQuestion.lean		ErwQuestion.lean
EuclideanSpace.lean		EuclideanSpace.lean
ExistsI.lean		ExistsI.lean
Explode.lean		Explode.lean
ExtractGoal.lean		ExtractGoal.lean
FBinop.lean		FBinop.lean
FieldSimp.lean		FieldSimp.lean
FinCoercions.lean		FinCoercions.lean
Find.lean		Find.lean
FindDeprecations.lean		FindDeprecations.lean
FindSyntax.lean		FindSyntax.lean
FlexibleLinter.lean		FlexibleLinter.lean
ForbiddenModuleNames.lean		ForbiddenModuleNames.lean
FunLike.lean		FunLike.lean
GRewrite.lean		GRewrite.lean
GalNotation.lean		GalNotation.lean
Group.lean		Group.lean
GuardGoalNums.lean		GuardGoalNums.lean
GuardHypNums.lean		GuardHypNums.lean
HashCommandLinter.lean		HashCommandLinter.lean
HashLint.lean		HashLint.lean
Have.lean		Have.lean
HaveLetLinter.lean		HaveLetLinter.lean
Header.lean		Header.lean
HeaderFail.lean		HeaderFail.lean
HigherOrder.lean		HigherOrder.lean
ImplicitUniverses.lean		ImplicitUniverses.lean
ImportHeavyFlexibleLinter.lean		ImportHeavyFlexibleLinter.lean
InferParam.lean		InferParam.lean
Inhabit.lean		Inhabit.lean
InstanceTransparency.lean		InstanceTransparency.lean
IsBoundedDefault.lean		IsBoundedDefault.lean
LibraryRewrite.lean		LibraryRewrite.lean
Lint.lean		Lint.lean
LintStyle.lean		LintStyle.lean
LongFile.lean		LongFile.lean
MathlibTestExecutable.lean		MathlibTestExecutable.lean

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

FilesExpand file tree

MathlibTest

Directory actions

More options

Directory actions

More options

Latest commit

History

MathlibTest

Folders and files

parent directory