DepRewrite
📁 Source: Mathlib/Tactic/DepRewrite.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsCastMode, toNat, Config, castMode, castTransparency, occs, transparency, Context, cfg, h, p, pHeadIdx, pNumArgs, x, Δ, δ, depRewriteTarget, depRw, depRwTarget, evalDepRewriteSeq, evalDepRwSeq, canUseCache, castBack?, castFwd, castMData, checkCastAllowed, cleanupCasts, dabstract, depRewriteLocalDecl, depRewriteSeq, depRewriteTarget, depRwLocalDecl, depRwSeq, depRwTarget, elabDepRewriteConfig, evalDepRewriteSeq, evalDepRwSeq, instBEqCastMode, beq, instDecidableLECastMode, instLECastMode, instToStringCastMode, visit, visitAndCast, visitInner, zetaDelta | 46 |
| 4 | |
| Total | 50 |
Mathlib.Tactic.DepRewrite
Definitions
| Name | Category | Theorems |
|---|---|---|
CastMode 📖 | CompData | — |
Config 📖 | CompData | — |
Context 📖 | CompData | — |
canUseCache 📖 | CompOp | — |
castBack? 📖 | CompOp | — |
castFwd 📖 | CompOp | — |
castMData 📖 | CompOp | — |
checkCastAllowed 📖 | CompOp | — |
cleanupCasts 📖 | CompOp | — |
dabstract 📖 | CompOp | — |
depRewriteLocalDecl 📖 | CompOp | — |
depRewriteSeq 📖 | CompOp | — |
depRewriteTarget 📖 | CompOp | — |
depRwLocalDecl 📖 | CompOp | — |
depRwSeq 📖 | CompOp | — |
depRwTarget 📖 | CompOp | — |
elabDepRewriteConfig 📖 | CompOp | — |
evalDepRewriteSeq 📖 | CompOp | — |
evalDepRwSeq 📖 | CompOp | — |
instBEqCastMode 📖 | CompOp | — |
instDecidableLECastMode 📖 | CompOp | — |
instLECastMode 📖 | CompOp | — |
instToStringCastMode 📖 | CompOp | — |
visit 📖 | CompOp | — |
visitAndCast 📖 | CompOp | — |
visitInner 📖 | CompOp | — |
zetaDelta 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
dcongrArg 📖 | — | — | — | — | — |
heqL 📖 | — | — | — | — | — |
heqR 📖 | — | — | — | — | — |
nddcongrArg 📖 | — | — | — | — | — |
Mathlib.Tactic.DepRewrite.CastMode
Definitions
| Name | Category | Theorems |
|---|---|---|
toNat 📖 | CompOp | — |
Mathlib.Tactic.DepRewrite.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
castMode 📖 | CompOp | — |
castTransparency 📖 | CompOp | — |
occs 📖 | CompOp | — |
transparency 📖 | CompOp | — |
Mathlib.Tactic.DepRewrite.Context
Definitions
| Name | Category | Theorems |
|---|---|---|
cfg 📖 | CompOp | — |
h 📖 | CompOp | — |
p 📖 | CompOp | — |
pHeadIdx 📖 | CompOp | — |
pNumArgs 📖 | CompOp | — |
x 📖 | CompOp | — |
Δ 📖 | CompOp | — |
δ 📖 | CompOp | — |
Mathlib.Tactic.DepRewrite.Conv
Definitions
| Name | Category | Theorems |
|---|---|---|
depRewriteTarget 📖 | CompOp | — |
depRw 📖 | CompOp | — |
depRwTarget 📖 | CompOp | — |
evalDepRewriteSeq 📖 | CompOp | — |
evalDepRwSeq 📖 | CompOp | — |
Mathlib.Tactic.DepRewrite.instBEqCastMode
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
---