Core
📁 Source: Mathlib/Tactic/NormNum/Core.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsEntry, NormNumExt, eval, name, post, pre, NormNums, erase, eraseCore, erased, tree, derive, deriveBool, deriveBoolOfIff, deriveInt, deriveNat, deriveRat, deriveSimp, discharge, elabNormNum, eval, getSimpContext, instInhabitedNormNums, default, methods, mkNormNumExt, normNumExt, tryNormNum, elabNormNum1Conv, elabNormNumConv, normNum, normNum1, normNum1Conv, normNumCmd, normNumConv | 35 |
| Theorems | 0 |
| Total | 35 |
Mathlib.Meta.NormNum
Definitions
| Name | Category | Theorems |
|---|---|---|
Entry 📖 | CompOp | — |
NormNumExt 📖 | CompData | — |
NormNums 📖 | CompData | — |
derive 📖 | CompOp | — |
deriveBool 📖 | CompOp | — |
deriveBoolOfIff 📖 | CompOp | — |
deriveInt 📖 | CompOp | — |
deriveNat 📖 | CompOp | — |
deriveRat 📖 | CompOp | — |
deriveSimp 📖 | CompOp | — |
discharge 📖 | CompOp | — |
elabNormNum 📖 | CompOp | — |
eval 📖 | CompOp | — |
getSimpContext 📖 | CompOp | — |
instInhabitedNormNums 📖 | CompOp | — |
methods 📖 | CompOp | — |
mkNormNumExt 📖 | CompOp | — |
normNumExt 📖 | CompOp | — |
tryNormNum 📖 | CompOp | — |
Mathlib.Meta.NormNum.NormNumExt
Definitions
| Name | Category | Theorems |
|---|---|---|
eval 📖 | CompOp | — |
name 📖 | CompOp | — |
post 📖 | CompOp | — |
pre 📖 | CompOp | — |
Mathlib.Meta.NormNum.NormNums
Definitions
| Name | Category | Theorems |
|---|---|---|
erase 📖 | CompOp | — |
eraseCore 📖 | CompOp | — |
erased 📖 | CompOp | — |
tree 📖 | CompOp | — |
Mathlib.Meta.NormNum.instInhabitedNormNums
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
elabNormNum1Conv 📖 | CompOp | — |
elabNormNumConv 📖 | CompOp | — |
normNum 📖 | CompOp | — |
normNum1 📖 | CompOp | — |
normNum1Conv 📖 | CompOp | — |
normNumCmd 📖 | CompOp | — |
normNumConv 📖 | CompOp | — |
---