Push
📁 Source: Mathlib/Tactic/Push.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsConfig, distrib, convPull____, convPush_____, convPush_neg_, elabDischarger, elabHead, elabPushConfig, elabPushTree, isUnderscore, pull, pullCommand, pullCore, pullStep, pushCommand, pushCore, pushNegCommand, pushSimpConfig, pushStep, pushStx, pushTree, use_distrib, resolvePushId?, pullFun, pushFun | 25 |
| 5 | |
| Total | 30 |
Mathlib.Tactic.Push
Definitions
| Name | Category | Theorems |
|---|---|---|
Config 📖 | CompData | — |
convPull____ 📖 | CompOp | — |
convPush_____ 📖 | CompOp | — |
convPush_neg_ 📖 | CompOp | — |
elabDischarger 📖 | CompOp | — |
elabHead 📖 | CompOp | — |
elabPushConfig 📖 | CompOp | — |
elabPushTree 📖 | CompOp | — |
isUnderscore 📖 | CompOp | — |
pull 📖 | CompOp | — |
pullCommand 📖 | CompOp | — |
pullCore 📖 | CompOp | — |
pullStep 📖 | CompOp | — |
pushCommand 📖 | CompOp | — |
pushCore 📖 | CompOp | — |
pushNegCommand 📖 | CompOp | — |
pushSimpConfig 📖 | CompOp | — |
pushStep 📖 | CompOp | — |
pushStx 📖 | CompOp | — |
pushTree 📖 | CompOp | — |
resolvePushId? 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
not_and_eq 📖 | — | — | — | — | — |
not_and_or_eq 📖 | — | — | — | — | not_and_or |
not_exists 📖 | — | — | — | — | — |
not_forall_eq 📖 | — | — | — | — | — |
not_iff 📖 | — | — | — | — | not_iffiff_iff_and_or_not_and_not |
Mathlib.Tactic.Push.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
distrib 📖 | CompOp | — |
Mathlib.Tactic.Push.push_neg
Definitions
| Name | Category | Theorems |
|---|---|---|
use_distrib 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
pullFun 📖 | CompOp | — |
pushFun 📖 | CompOp | — |
---