Init
📁 Source: Batteries/Tactic/Init.lean
Statistics
| Metric | Count |
|---|---|
Definitionsequals, exact, byContra, exacts, tacticAbsurd_, tacticBy_contra_core, tacticEapply_, tacticFapply_, tacticSplit_ands, tactic_, triv | 11 |
| Theorems | 0 |
| Total | 11 |
Batteries.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
byContra 📖 | CompOp | — |
exacts 📖 | CompOp | — |
tacticAbsurd_ 📖 | CompOp | — |
tacticBy_contra_core 📖 | CompOp | — |
tacticEapply_ 📖 | CompOp | — |
tacticFapply_ 📖 | CompOp | — |
tacticSplit_ands 📖 | CompOp | — |
tactic_ 📖 | CompOp | — |
triv 📖 | CompOp | — |
Batteries.Tactic.Conv
Definitions
| Name | Category | Theorems |
|---|---|---|
equals 📖 | CompOp | — |
exact 📖 | CompOp | — |
---