StacksAttribute
📁 Source: Mathlib/Tactic/StacksAttribute.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsstacksTagDB, formatter, parenthesizer, getStacksTag, Database, Tag, comment, database, declName, tag, addTagEntry, instBEqDatabase, beq, instBEqTag, beq, instHashableDatabase, hash, instHashableTag, hash, kerodonTags, stacksTag, quot, stacksTagDBKerodon, stacksTagDBStacks, stacksTagFn, stacksTagKind, stacksTagNoAntiquot, stacksTagParser, stacksTags, tagExt, traceStacksTags | 31 |
| Theorems | 0 |
| Total | 31 |
Lean.Parser.Category
Definitions
| Name | Category | Theorems |
|---|---|---|
stacksTagDB 📖 | CompOp | — |
Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot
Definitions
| Name | Category | Theorems |
|---|---|---|
formatter 📖 | CompOp | — |
Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot
Definitions
| Name | Category | Theorems |
|---|---|---|
parenthesizer 📖 | CompOp | — |
Lean.TSyntax
Definitions
| Name | Category | Theorems |
|---|---|---|
getStacksTag 📖 | CompOp | — |
Mathlib.StacksTag
Definitions
| Name | Category | Theorems |
|---|---|---|
Database 📖 | CompData | — |
Tag 📖 | CompData | — |
addTagEntry 📖 | CompOp | — |
instBEqDatabase 📖 | CompOp | — |
instBEqTag 📖 | CompOp | — |
instHashableDatabase 📖 | CompOp | — |
instHashableTag 📖 | CompOp | — |
kerodonTags 📖 | CompOp | — |
stacksTag 📖 | CompOp | — |
stacksTagDBKerodon 📖 | CompOp | — |
stacksTagDBStacks 📖 | CompOp | — |
stacksTagFn 📖 | CompOp | — |
stacksTagKind 📖 | CompOp | — |
stacksTagNoAntiquot 📖 | CompOp | — |
stacksTagParser 📖 | CompOp | — |
stacksTags 📖 | CompOp | — |
tagExt 📖 | CompOp | — |
traceStacksTags 📖 | CompOp | — |
Mathlib.StacksTag.Tag
Definitions
| Name | Category | Theorems |
|---|---|---|
comment 📖 | CompOp | — |
database 📖 | CompOp | — |
declName 📖 | CompOp | — |
tag 📖 | CompOp | — |
Mathlib.StacksTag.instBEqDatabase
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.StacksTag.instBEqTag
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.StacksTag.instHashableDatabase
Definitions
| Name | Category | Theorems |
|---|---|---|
hash 📖 | CompOp | — |
Mathlib.StacksTag.instHashableTag
Definitions
| Name | Category | Theorems |
|---|---|---|
hash 📖 | CompOp | — |
Mathlib.StacksTag.stacksTagDB
Definitions
| Name | Category | Theorems |
|---|---|---|
quot 📖 | CompOp | — |
---