Types
📁 Source: Mathlib/Tactic/FunProp/Types.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsConfig, maxSteps, maxTransitionDepth, Context, config, constToUnfold, disch, increaseTransitionDepth, transitionDepth, FunPropM, getFnOrigin, GeneralTheorem, funPropName, keys, priority, thmName, GeneralTheorems, theorems, Origin, getValue, name, proof, cache, failureCache, morTheorems, msgLog, numSteps, transitionTheorems, defaultNamesToUnfold, defaultUnfoldPred, increaseSteps, instBEqConfig, beq, instBEqOrigin, beq, instInhabitedConfig, default, instInhabitedGeneralTheorem, default, instInhabitedGeneralTheorems, default, instInhabitedOrigin, default, logError, ppOrigin, ppOrigin', unfoldNamePred, withIncreasedTransitionDepth | 48 |
| Theorems | 0 |
| Total | 48 |
Mathlib.Meta.FunProp
Definitions
| Name | Category | Theorems |
|---|---|---|
Config 📖 | CompData | — |
Context 📖 | CompData | — |
FunPropM 📖 | CompOp | — |
GeneralTheorem 📖 | CompData | — |
GeneralTheorems 📖 | CompData | — |
Origin 📖 | CompData | — |
defaultNamesToUnfold 📖 | CompOp | — |
defaultUnfoldPred 📖 | CompOp | — |
increaseSteps 📖 | CompOp | — |
instBEqConfig 📖 | CompOp | — |
instBEqOrigin 📖 | CompOp | — |
instInhabitedConfig 📖 | CompOp | — |
instInhabitedGeneralTheorem 📖 | CompOp | — |
instInhabitedGeneralTheorems 📖 | CompOp | — |
instInhabitedOrigin 📖 | CompOp | — |
logError 📖 | CompOp | — |
ppOrigin 📖 | CompOp | — |
ppOrigin' 📖 | CompOp | — |
unfoldNamePred 📖 | CompOp | — |
withIncreasedTransitionDepth 📖 | CompOp | — |
Mathlib.Meta.FunProp.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
maxSteps 📖 | CompOp | — |
maxTransitionDepth 📖 | CompOp | — |
Mathlib.Meta.FunProp.Context
Definitions
| Name | Category | Theorems |
|---|---|---|
config 📖 | CompOp | — |
constToUnfold 📖 | CompOp | — |
disch 📖 | CompOp | — |
increaseTransitionDepth 📖 | CompOp | — |
transitionDepth 📖 | CompOp | — |
Mathlib.Meta.FunProp.FunctionData
Definitions
| Name | Category | Theorems |
|---|---|---|
getFnOrigin 📖 | CompOp | — |
Mathlib.Meta.FunProp.GeneralTheorem
Definitions
| Name | Category | Theorems |
|---|---|---|
funPropName 📖 | CompOp | — |
keys 📖 | CompOp | — |
priority 📖 | CompOp | — |
thmName 📖 | CompOp | — |
Mathlib.Meta.FunProp.GeneralTheorems
Definitions
| Name | Category | Theorems |
|---|---|---|
theorems 📖 | CompOp | — |
Mathlib.Meta.FunProp.Origin
Definitions
| Name | Category | Theorems |
|---|---|---|
getValue 📖 | CompOp | — |
name 📖 | CompOp | — |
Mathlib.Meta.FunProp.Result
Definitions
| Name | Category | Theorems |
|---|---|---|
proof 📖 | CompOp | — |
Mathlib.Meta.FunProp.State
Definitions
| Name | Category | Theorems |
|---|---|---|
cache 📖 | CompOp | — |
failureCache 📖 | CompOp | — |
morTheorems 📖 | CompOp | — |
msgLog 📖 | CompOp | — |
numSteps 📖 | CompOp | — |
transitionTheorems 📖 | CompOp | — |
Mathlib.Meta.FunProp.instBEqConfig
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.Meta.FunProp.instBEqOrigin
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedConfig
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedGeneralTheorem
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedGeneralTheorems
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedOrigin
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---