OpenPrivate
📁 Source: Batteries/Tactic/OpenPrivate.lean
Statistics
| Metric | Count |
|---|---|
| 9 | |
| Theorems | 0 |
| Total | 9 |
Lean
Definitions
| Name | Category | Theorems |
|---|---|---|
instDecidableEqModuleIdx_batteries 📖 | CompOp | — |
Lean.Elab
Definitions
| Name | Category | Theorems |
|---|---|---|
addModuleInfo 📖 | CompOp | — |
Lean.Elab.Command
Definitions
| Name | Category | Theorems |
|---|---|---|
elabExportPrivate 📖 | CompOp | — |
elabOpenPrivate 📖 | CompOp | — |
elabOpenPrivateLike 📖 | CompOp | — |
exportPrivate 📖 | CompOp | — |
Lean.Environment
Definitions
| Name | Category | Theorems |
|---|---|---|
declsInModuleIdx 📖 | CompOp | — |
moduleIdxForModule? 📖 | CompOp | — |
Lean.Meta
Definitions
| Name | Category | Theorems |
|---|---|---|
collectPrivateIn 📖 | CompOp | — |
---