Documentation Verification Report

Core

📁 Source: Mathlib/Tactic/Translate/Core.lean

Statistics

MetricCount
DefinitionsCore, Config, allowAutoName, attrs, doc, dontTranslate, existing, none, ref, relevantArg?, reorder?, self, tgt, swapFirstTwo, RelevantArg, Reorder, ReplacementM, run, TranslateData, attrName, changeNumeral, doTranslateAttr, guessNameData, ignoreArgsAttr, isDual, translations, unfoldBoundaries?, TranslationInfo, relevantArg, reorder, translation, addTranslationAttr, applyAttributes, applyReplacementForall, applyReplacementFun, applyReplacementLambda, attrArgs, attrOption, bracketedOption, checkExistingType, copyInstanceAttribute, copyMetaData, declUnfoldSimpAuxLemmas, dontTranslateOption, elabArgStx, elabTranslationAttr, etaExpandN, findAuxDecls, findPrefixTranslation?, findTargetName, findTranslation?, findTranslationName?, getRelevantArg, guessReorder, insertTranslation, instBEqRelevantArg, beq, instInhabitedRelevantArg, default, instToMessageDataRelevantArg, existingAttributeWarning, translateExisting, translateGenerateName, translateOverwrite, translateRedundant, translateRelevantArg, translateReorder, proceedFields, proceedFieldsAux, relevantArgOption, renameBinderNames, reorderForall, reorderLambda, reorderOption, shouldTranslate, targetName, transformDeclRec, translateLemmas, translationHint, updateAndAddDecl, updateDecl, warnAttr, warnAttrCore, warnParametricAttr, Core, Core, Core, Core
88
Theorems0
Total88

InnerProductSpace

Definitions

NameCategoryTheorems
Core 📖CompData

Mathlib.Tactic.Translate

Definitions

NameCategoryTheorems
Config 📖CompData
RelevantArg 📖CompData
Reorder 📖CompOp
ReplacementM 📖CompOp
TranslateData 📖CompData
TranslationInfo 📖CompData
addTranslationAttr 📖CompOp
applyAttributes 📖CompOp
applyReplacementForall 📖CompOp
applyReplacementFun 📖CompOp
applyReplacementLambda 📖CompOp
attrArgs 📖CompOp
attrOption 📖CompOp
bracketedOption 📖CompOp
checkExistingType 📖CompOp
copyInstanceAttribute 📖CompOp
copyMetaData 📖CompOp
declUnfoldSimpAuxLemmas 📖CompOp
dontTranslateOption 📖CompOp
elabArgStx 📖CompOp
elabTranslationAttr 📖CompOp
etaExpandN 📖CompOp
findAuxDecls 📖CompOp
findPrefixTranslation? 📖CompOp
findTargetName 📖CompOp
findTranslation? 📖CompOp
findTranslationName? 📖CompOp
getRelevantArg 📖CompOp
guessReorder 📖CompOp
insertTranslation 📖CompOp
instBEqRelevantArg 📖CompOp
instInhabitedRelevantArg 📖CompOp
instToMessageDataRelevantArg 📖CompOp
proceedFields 📖CompOp
proceedFieldsAux 📖CompOp
relevantArgOption 📖CompOp
renameBinderNames 📖CompOp
reorderForall 📖CompOp
reorderLambda 📖CompOp
reorderOption 📖CompOp
shouldTranslate 📖CompOp
targetName 📖CompOp
transformDeclRec 📖CompOp
translateLemmas 📖CompOp
translationHint 📖CompOp
updateAndAddDecl 📖CompOp
updateDecl 📖CompOp
warnAttr 📖CompOp
warnAttrCore 📖CompOp
warnParametricAttr 📖CompOp

Mathlib.Tactic.Translate.Config

Definitions

NameCategoryTheorems
allowAutoName 📖CompOp
attrs 📖CompOp
doc 📖CompOp
dontTranslate 📖CompOp
existing 📖CompOp
none 📖CompOp
ref 📖CompOp
relevantArg? 📖CompOp
reorder? 📖CompOp
self 📖CompOp
tgt 📖CompOp

Mathlib.Tactic.Translate.List

Definitions

NameCategoryTheorems
swapFirstTwo 📖CompOp

Mathlib.Tactic.Translate.ReplacementM

Definitions

NameCategoryTheorems
run 📖CompOp

Mathlib.Tactic.Translate.TranslateData

Definitions

NameCategoryTheorems
attrName 📖CompOp
changeNumeral 📖CompOp
doTranslateAttr 📖CompOp
guessNameData 📖CompOp
ignoreArgsAttr 📖CompOp
isDual 📖CompOp
translations 📖CompOp
unfoldBoundaries? 📖CompOp

Mathlib.Tactic.Translate.TranslationInfo

Definitions

NameCategoryTheorems
relevantArg 📖CompOp
reorder 📖CompOp
translation 📖CompOp

Mathlib.Tactic.Translate.instBEqRelevantArg

Definitions

NameCategoryTheorems
beq 📖CompOp

Mathlib.Tactic.Translate.instInhabitedRelevantArg

Definitions

NameCategoryTheorems
default 📖CompOp

Mathlib.Tactic.Translate.linter

Definitions

NameCategoryTheorems
existingAttributeWarning 📖CompOp
translateExisting 📖CompOp
translateGenerateName 📖CompOp
translateOverwrite 📖CompOp
translateRedundant 📖CompOp
translateRelevantArg 📖CompOp
translateReorder 📖CompOp

NormedSpace

Definitions

NameCategoryTheorems
Core 📖CompData
3 mathmath: CStarModule.normedSpaceCore, InnerProductSpace.Core.toNormedSpaceCore, CStarMatrix.normedSpaceCore

PreInnerProductSpace

Definitions

NameCategoryTheorems
Core 📖CompData

SeminormedSpace

Definitions

NameCategoryTheorems
Core 📖CompData
2 mathmath: NormedSpace.Core.toCore, InnerProductSpace.Core.toSeminormedSpaceCore

UniformSpace

Definitions

NameCategoryTheorems
Core 📖CompData

---

← Back to Index