Basic

📁 Source: Mathlib/Tactic/Simps/Basic.lean

Statistics

Metric	Count
Definitions instantiateLambdasOrApps, mkSimpContext, mkSimpContextResult, attrSimps!?_, attrSimps!_, attrSimps?!_, attrSimps?_, simps, simpsArgsRest, commandInitialize_simps_projections?_, initialize_simps_projections, simpsProj, simpsRule, add, erase, prefix, rename, simpsNoConstructor, simpsUnusedCustomDeclarations, custom_simps_projection, Config, attrs, debug, fullyApplied, isSimp, nameStem, notRecursive, rhsMd, simpRhs, typeMd, ParsedProjectionData, expr?, isCustom, isDefault, isPrefix, newName, newStx, projNrs, strName, strStx, toProjectionData, ProjectionData, expr, isDefault, isPrefix, name, projNrs, ProjectionRule, addProjection, addProjections, applyProjectionRules, checkForUnusedCustomProjs, elabInitializeSimpsProjections, elabSimpsConfig, elabSimpsRule, findAutomaticProjections, findAutomaticProjectionsAux, findProjection, findProjectionIndices, getCompositeOfProjections, getCompositeOfProjectionsAux, getProjectionExprs, getRawProjections, headStructureEtaReduce, instInhabitedConfig, default, instInhabitedProjectionData, default, instToMessageDataParsedProjectionData, instToMessageDataProjectionData, instToMessageDataProjectionRule, mkParsedProjectionData, projectionsInfo, structureExt, instCoeNameStructName, simpsAttr, simpsTac, simpsTacFromSyntax	78
Theorems	0
Total	78

Lean.Expr

Definitions

Name	Category	Theorems
instantiateLambdasOrApps 📖	CompOp	—

Lean.Meta

Definitions

Name	Category	Theorems
mkSimpContext 📖	CompOp	—
mkSimpContextResult 📖	CompOp	—

Lean.Parser.Attr

Definitions

Name	Category	Theorems
attrSimps!?_ 📖	CompOp	—
attrSimps!_ 📖	CompOp	—
attrSimps?!_ 📖	CompOp	—
attrSimps?_ 📖	CompOp	—
simps 📖	CompOp	—
simpsArgsRest 📖	CompOp	—

Lean.Parser.Command

Definitions

Name	Category	Theorems
commandInitialize_simps_projections?_ 📖	CompOp	—
initialize_simps_projections 📖	CompOp	—
simpsProj 📖	CompOp	—
simpsRule 📖	CompOp	—

Lean.Parser.Command.simpsRule

Definitions

Name	Category	Theorems
add 📖	CompOp	—
erase 📖	CompOp	—
prefix 📖	CompOp	—
rename 📖	CompOp	—

Lean.Parser.linter

Definitions

Name	Category	Theorems
simpsNoConstructor 📖	CompOp	—
simpsUnusedCustomDeclarations 📖	CompOp	—

LibraryNote

Definitions

Name	Category	Theorems
custom_simps_projection 📖	CompOp	—

Simps

Definitions

Name	Category	Theorems
Config 📖	CompData	—
ParsedProjectionData 📖	CompData	—
ProjectionData 📖	CompData	—
ProjectionRule 📖	CompData	—
addProjection 📖	CompOp	—
addProjections 📖	CompOp	—
applyProjectionRules 📖	CompOp	—
checkForUnusedCustomProjs 📖	CompOp	—
elabInitializeSimpsProjections 📖	CompOp	—
elabSimpsConfig 📖	CompOp	—
elabSimpsRule 📖	CompOp	—
findAutomaticProjections 📖	CompOp	—
findAutomaticProjectionsAux 📖	CompOp	—
findProjection 📖	CompOp	—
findProjectionIndices 📖	CompOp	—
getCompositeOfProjections 📖	CompOp	—
getCompositeOfProjectionsAux 📖	CompOp	—
getProjectionExprs 📖	CompOp	—
getRawProjections 📖	CompOp	—
headStructureEtaReduce 📖	CompOp	—
instInhabitedConfig 📖	CompOp	—
instInhabitedProjectionData 📖	CompOp	—
instToMessageDataParsedProjectionData 📖	CompOp	—
instToMessageDataProjectionData 📖	CompOp	—
instToMessageDataProjectionRule 📖	CompOp	—
mkParsedProjectionData 📖	CompOp	—
projectionsInfo 📖	CompOp	—
structureExt 📖	CompOp	—

Simps.Config

Definitions

Name	Category	Theorems
attrs 📖	CompOp	—
debug 📖	CompOp	—
fullyApplied 📖	CompOp	—
isSimp 📖	CompOp	—
nameStem 📖	CompOp	—
notRecursive 📖	CompOp	—
rhsMd 📖	CompOp	—
simpRhs 📖	CompOp	—
typeMd 📖	CompOp	—

Simps.ParsedProjectionData

Definitions

Name	Category	Theorems
expr? 📖	CompOp	—
isCustom 📖	CompOp	—
isDefault 📖	CompOp	—
isPrefix 📖	CompOp	—
newName 📖	CompOp	—
newStx 📖	CompOp	—
projNrs 📖	CompOp	—
strName 📖	CompOp	—
strStx 📖	CompOp	—
toProjectionData 📖	CompOp	—

Simps.ProjectionData

Definitions

Name	Category	Theorems
expr 📖	CompOp	—
isDefault 📖	CompOp	—
isPrefix 📖	CompOp	—
name 📖	CompOp	—
projNrs 📖	CompOp	—

Simps.instInhabitedConfig

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Simps.instInhabitedProjectionData

Definitions

Name	Category	Theorems
default 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instCoeNameStructName 📖	CompOp	—
simpsAttr 📖	CompOp	—
simpsTac 📖	CompOp	—
simpsTacFromSyntax 📖	CompOp	—

---

← Back to Index