Basic
📁 Source: Mathlib/Lean/Expr/Basic.lean
Statistics
Lean
Definitions
| Name | Category | Theorems |
|---|---|---|
getFieldsToParents 📖 | CompOp | — |
mkConst' 📖 | CompOp | — |
Lean.BinderInfo
Definitions
| Name | Category | Theorems |
|---|---|---|
brackets 📖 | CompOp | — |
Lean.ConstantInfo
Definitions
| Name | Category | Theorems |
|---|---|---|
isDef 📖 | CompOp | — |
isThm 📖 | CompOp | — |
toDeclaration! 📖 | CompOp | — |
updateConstantVal 📖 | CompOp | — |
updateLevelParams 📖 | CompOp | — |
updateName 📖 | CompOp | — |
updateType 📖 | CompOp | — |
updateValue 📖 | CompOp | — |
Lean.Expr
Definitions
| Name | Category | Theorems |
|---|---|---|
bvarIdx? 📖 | CompOp | — |
containsConst 📖 | CompOp | — |
ensureHasNoMVars 📖 | CompOp | — |
eraseProofs 📖 | CompOp | — |
forallNot_of_notExists 📖 | CompOp | — |
getAppApps 📖 | CompOp | — |
getArg? 📖 | CompOp | — |
getBinderName 📖 | CompOp | — |
getRevArg? 📖 | CompOp | — |
getUnusedForallInstanceBinderIdxsWhere 📖 | CompOp | — |
isAppOrForallOfConst 📖 | CompOp | — |
isAppOrForallOfConstP 📖 | CompOp | — |
isConstantApplication 📖 | CompOp | — |
le? 📖 | CompOp | — |
letDepth 📖 | CompOp | — |
lt? 📖 | CompOp | — |
mapForallBinderNames 📖 | CompOp | — |
mkDirectProjection 📖 | CompOp | — |
mkProjection 📖 | CompOp | — |
modifyAppArgM 📖 | CompOp | — |
modifyArg 📖 | CompOp | — |
modifyArgM 📖 | CompOp | — |
modifyRevArg 📖 | CompOp | — |
ne?' 📖 | CompOp | — |
numeral? 📖 | CompOp | — |
ofInt 📖 | CompOp | — |
ofNat 📖 | CompOp | — |
reduceProjStruct? 📖 | CompOp | — |
renameBVar 📖 | CompOp | — |
setArg 📖 | CompOp | — |
sides? 📖 | CompOp | — |
type? 📖 | CompOp | — |
zero? 📖 | CompOp | — |
Lean.Name
Definitions
| Name | Category | Theorems |
|---|---|---|
fromComponents 📖 | CompOp | — |
isBlackListed 📖 | CompOp | — |
isPrefixOf? 📖 | CompOp | — |
lastComponentAsString 📖 | CompOp | — |
mapPrefix 📖 | CompOp | — |
splitAt 📖 | CompOp | — |
updateLast 📖 | CompOp | — |
---