Core
📁 Source: Mathlib/Tactic/GRewrite/Core.lean
Statistics
| Metric | Count |
|---|---|
Definitionsgrewrite, Config, implicationHyp, toConfig, useRewrite, dischargeMain, GRewriteResult, eNew, impProof, mvarIds | 10 |
| Theorems | 0 |
| Total | 10 |
Lean.MVarId
Definitions
| Name | Category | Theorems |
|---|---|---|
grewrite 📖 | CompOp | — |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
GRewriteResult 📖 | CompData | — |
Mathlib.Tactic.GRewrite
Definitions
| Name | Category | Theorems |
|---|---|---|
Config 📖 | CompData | — |
dischargeMain 📖 | CompOp | — |
Mathlib.Tactic.GRewrite.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
implicationHyp 📖 | CompOp | — |
toConfig 📖 | CompOp | — |
useRewrite 📖 | CompOp | — |
Mathlib.Tactic.GRewriteResult
Definitions
| Name | Category | Theorems |
|---|---|---|
eNew 📖 | CompOp | — |
impProof 📖 | CompOp | — |
mvarIds 📖 | CompOp | — |
---