Expr
📁 Source: Batteries/Lean/Expr.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsaddLocalVarInfoForBinderIdent, getAppArgs', getAppRevArgs', getArgD', getRevArgD', intLit!, isAppOf', natLit!, toSyntax, traverseApp', withApp', go, withAppRev', go | 14 |
| Theorems | 0 |
| Total | 14 |
Lean.Expr
Definitions
| Name | Category | Theorems |
|---|---|---|
addLocalVarInfoForBinderIdent 📖 | CompOp | — |
getAppArgs' 📖 | CompOp | — |
getAppRevArgs' 📖 | CompOp | — |
getArgD' 📖 | CompOp | — |
getRevArgD' 📖 | CompOp | — |
intLit! 📖 | CompOp | — |
isAppOf' 📖 | CompOp | — |
natLit! 📖 | CompOp | — |
toSyntax 📖 | CompOp | — |
traverseApp' 📖 | CompOp | — |
withApp' 📖 | CompOp | — |
withAppRev' 📖 | CompOp | — |
Lean.Expr.withApp'
Definitions
| Name | Category | Theorems |
|---|---|---|
go 📖 | CompOp | — |
Lean.Expr.withAppRev'
Definitions
| Name | Category | Theorems |
|---|---|---|
go 📖 | CompOp | — |
---