Basic
📁 Source: PhysLean/Meta/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsflatFilterSizeM, flatSize, fileName, getDeclString, getDeclStringNoDoc, getDocString, hasDocString, hasPos, lineNumber, location, toFilePath, toGitHubLink, toRelativeFilePath, getConsts, getLines, getUserConsts, allDocStrings, allImports, allUserConsts, noDefs, noDefsNoDocString, noFilesWithTODOs, noImports, noLemmas, noLemmasNoDocString, noLines, noTODOs | 27 |
| Theorems | 0 |
| Total | 27 |
Array
Definitions
| Name | Category | Theorems |
|---|---|---|
flatFilterSizeM 📖 | CompOp | — |
flatSize 📖 | CompOp | — |
Lean.Name
Definitions
| Name | Category | Theorems |
|---|---|---|
fileName 📖 | CompOp | — |
getDeclString 📖 | CompOp | — |
getDeclStringNoDoc 📖 | CompOp | — |
getDocString 📖 | CompOp | — |
hasDocString 📖 | CompOp | — |
hasPos 📖 | CompOp | — |
lineNumber 📖 | CompOp | — |
location 📖 | CompOp | — |
toFilePath 📖 | CompOp | — |
toGitHubLink 📖 | CompOp | — |
toRelativeFilePath 📖 | CompOp | — |
PhysLean
Definitions
| Name | Category | Theorems |
|---|---|---|
allDocStrings 📖 | CompOp | — |
allImports 📖 | CompOp | — |
allUserConsts 📖 | CompOp | — |
noDefs 📖 | CompOp | — |
noDefsNoDocString 📖 | CompOp | — |
noFilesWithTODOs 📖 | CompOp | — |
noImports 📖 | CompOp | — |
noLemmas 📖 | CompOp | — |
noLemmasNoDocString 📖 | CompOp | — |
noLines 📖 | CompOp | — |
noTODOs 📖 | CompOp | — |
PhysLean.Imports
Definitions
| Name | Category | Theorems |
|---|---|---|
getConsts 📖 | CompOp | — |
getLines 📖 | CompOp | — |
getUserConsts 📖 | CompOp | — |
---