MkIffOfInductiveProp
📁 Source: Mathlib/Tactic/MkIffOfInductiveProp.lean
Statistics
| Metric | Count |
|---|---|
| 19 | |
| Theorems | 0 |
| Total | 19 |
Mathlib.Tactic.MkIff
Definitions
| Name | Category | Theorems |
|---|---|---|
Shape 📖 | CompData | — |
compactRelation 📖 | CompOp | — |
constrToProp 📖 | CompOp | — |
listBoolMerge 📖 | CompOp | — |
mkAndList 📖 | CompOp | — |
mkExistsList 📖 | CompOp | — |
mkIff 📖 | CompOp | — |
mkIffOfInductiveProp 📖 | CompOp | — |
mkIffOfInductivePropImpl 📖 | CompOp | — |
mkOpList 📖 | CompOp | — |
mkOrList 📖 | CompOp | — |
nCasesProd 📖 | CompOp | — |
nCasesSum 📖 | CompOp | — |
splitThenConstructor 📖 | CompOp | — |
toCases 📖 | CompOp | — |
toInductive 📖 | CompOp | — |
Mathlib.Tactic.MkIff.List
Definitions
| Name | Category | Theorems |
|---|---|---|
init 📖 | CompOp | — |
Mathlib.Tactic.MkIff.Shape
Definitions
| Name | Category | Theorems |
|---|---|---|
neqs 📖 | CompOp | — |
variablesKept 📖 | CompOp | — |
---