📁 Source: Mathlib/Util/Qq.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsfindLocalDeclWithTypeQ?, getLevelQ, getLevelQ', inferTypeQ', mkDecideProofQ, mkIntLitQ, mkNatLitQ, mkSetLiteralQ | 8 |
Theoremsrfl | 1 |
| Total | 9 |
Definitions
| Name | Category | Theorems |
|---|---|---|
findLocalDeclWithTypeQ? 📖 | CompOp | — |
getLevelQ 📖 | CompOp | — |
getLevelQ' 📖 | CompOp | — |
inferTypeQ' 📖 | CompOp | — |
mkDecideProofQ 📖 | CompOp | — |
mkIntLitQ 📖 | CompOp | — |
mkNatLitQ 📖 | CompOp | — |
mkSetLiteralQ 📖 | CompOp | — |
Qq.QuotedDefEq
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
rfl 📖 | mathematical | — | Qq.QuotedDefEq | — | — |
---