ITauto
📁 Source: Mathlib/Tactic/ITauto.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsAndKind, cmp, sides, Context, add, format, withAdd, IProp, and, cmp, eq, format, iff, not, xor, Proof, app, exfalso, format, orElim, applyProof, freshName, instDecidableEqAndKind, instDecidableLTIProp, instInhabitedAndKind, instInhabitedIProp, instInhabitedProof, instLTIProp, instToExprAndKind, toExpr, instToExprIProp, toExpr, instToExprProof, toExpr, instToFormatContext, instToFormatIProp, instToFormatProof, isOk, itauto!, itautoCore, mapProof, prove, reify, search, whenOk | 45 |
| Theorems | 0 |
| Total | 45 |
Mathlib.Tactic.ITauto
Definitions
| Name | Category | Theorems |
|---|---|---|
AndKind 📖 | CompData | — |
Context 📖 | CompOp | — |
IProp 📖 | CompData | — |
Proof 📖 | CompData | — |
applyProof 📖 | CompOp | — |
freshName 📖 | CompOp | — |
instDecidableEqAndKind 📖 | CompOp | — |
instDecidableLTIProp 📖 | CompOp | — |
instInhabitedAndKind 📖 | CompOp | — |
instInhabitedIProp 📖 | CompOp | — |
instInhabitedProof 📖 | CompOp | — |
instLTIProp 📖 | CompOp | — |
instToExprAndKind 📖 | CompOp | — |
instToExprIProp 📖 | CompOp | — |
instToExprProof 📖 | CompOp | — |
instToFormatContext 📖 | CompOp | — |
instToFormatIProp 📖 | CompOp | — |
instToFormatProof 📖 | CompOp | — |
isOk 📖 | CompOp | — |
itauto! 📖 | CompOp | — |
itautoCore 📖 | CompOp | — |
mapProof 📖 | CompOp | — |
prove 📖 | CompOp | — |
reify 📖 | CompOp | — |
search 📖 | CompOp | — |
whenOk 📖 | CompOp | — |
Mathlib.Tactic.ITauto.AndKind
Definitions
| Name | Category | Theorems |
|---|---|---|
cmp 📖 | CompOp | — |
sides 📖 | CompOp | — |
Mathlib.Tactic.ITauto.Context
Definitions
| Name | Category | Theorems |
|---|---|---|
add 📖 | CompOp | — |
format 📖 | CompOp | — |
withAdd 📖 | CompOp | — |
Mathlib.Tactic.ITauto.IProp
Definitions
| Name | Category | Theorems |
|---|---|---|
and 📖 | CompOp | — |
cmp 📖 | CompOp | — |
eq 📖 | CompOp | — |
format 📖 | CompOp | — |
iff 📖 | CompOp | — |
not 📖 | CompOp | — |
xor 📖 | CompOp | — |
Mathlib.Tactic.ITauto.Proof
Definitions
| Name | Category | Theorems |
|---|---|---|
app 📖 | CompOp | — |
exfalso 📖 | CompOp | — |
format 📖 | CompOp | — |
orElim 📖 | CompOp | — |
Mathlib.Tactic.ITauto.instToExprAndKind
Definitions
| Name | Category | Theorems |
|---|---|---|
toExpr 📖 | CompOp | — |
Mathlib.Tactic.ITauto.instToExprIProp
Definitions
| Name | Category | Theorems |
|---|---|---|
toExpr 📖 | CompOp | — |
Mathlib.Tactic.ITauto.instToExprProof
Definitions
| Name | Category | Theorems |
|---|---|---|
toExpr 📖 | CompOp | — |
---