LibraryRewrite
📁 Source: Mathlib/Tactic/Widget/LibraryRewrite.lean
Statistics
Mathlib.Tactic.LibraryRewrite
Definitions
| Name | Category | Theorems |
|---|---|---|
Kind 📖 | CompData | — |
LibraryRewriteComponent 📖 | CompOp | — |
RewriteInterface 📖 | CompData | — |
RewriteLemma 📖 | CompData | — |
SectionToMessageData 📖 | CompOp | — |
addLocalRewriteEntry 📖 | CompOp | — |
addRewriteEntry 📖 | CompOp | — |
checkAndSortRewriteLemmas 📖 | CompOp | — |
checkRewrite 📖 | CompOp | — |
elabrw??Command 📖 | CompOp | — |
eqOrIff? 📖 | CompOp | — |
filterRewrites 📖 | CompOp | — |
getBinderInfos 📖 | CompOp | — |
getHypotheses 📖 | CompOp | — |
getHypothesisRewrites 📖 | CompOp | — |
getImportCandidates 📖 | CompOp | — |
getImportRewrites 📖 | CompOp | — |
getModuleCandidates 📖 | CompOp | — |
getModuleRewrites 📖 | CompOp | — |
getRewriteInterfaces 📖 | CompOp | — |
instBEqRewriteLemma 📖 | CompOp | — |
instInhabitedRewriteLemma 📖 | CompOp | — |
instToFormatRewriteLemma 📖 | CompOp | — |
isExplicitEq 📖 | CompOp | — |
isMVarSwap 📖 | CompOp | — |
pattern 📖 | CompOp | — |
renderRewrites 📖 | CompOp | — |
rpc 📖 | CompOp | — |
rw??Command 📖 | CompOp | — |
tacticRw?? 📖 | CompOp | — |
tacticSyntax 📖 | CompOp | — |
Mathlib.Tactic.LibraryRewrite.Rewrite
Definitions
| Name | Category | Theorems |
|---|---|---|
extraGoals 📖 | CompOp | — |
makesNewMVars 📖 | CompOp | — |
proof 📖 | CompOp | — |
replacement 📖 | CompOp | — |
stringLength 📖 | CompOp | — |
toInterface 📖 | CompOp | — |
toMessageData 📖 | CompOp | — |
Mathlib.Tactic.LibraryRewrite.RewriteInterface
Definitions
| Name | Category | Theorems |
|---|---|---|
extraGoals 📖 | CompOp | — |
lemmaType 📖 | CompOp | — |
makesNewMVars 📖 | CompOp | — |
prettyLemma 📖 | CompOp | — |
replacement 📖 | CompOp | — |
replacementString 📖 | CompOp | — |
tactic 📖 | CompOp | — |
Mathlib.Tactic.LibraryRewrite.RewriteLemma
Definitions
| Name | Category | Theorems |
|---|---|---|
name 📖 | CompOp | — |
Mathlib.Tactic.LibraryRewrite.instBEqRewriteLemma
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.Tactic.LibraryRewrite.instInhabitedRewriteLemma
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---