Notation3
📁 Source: Mathlib/Util/Notation3.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsBoundValueType, DelabKey, key, MatchState, captureSubexpr, delabVar, empty, foldState, getBinders, getFoldArray, pushFold, scopeState, vars, withVar, Matcher, bindersItem, expandFoldl, expandFoldr, exprToMatcher, foldAction, foldKind, getPrettyPrintOpt, identOptScoped, instInhabitedMatcher, instReprDelabKey, repr, isType', matchApp, matchExpr, matchFVar, matchFoldl, matchForall, matchLambda, matchScoped, matchTypeOf, matchVar, mkExprMatcher, mkFoldlMatcher, mkFoldrMatcher, mkScopedMatcher, natLitMatcher, notation3Item, prettyPrintOpt, setupLCtx, withHeadRefIfTagAppFns, «termExpand_binders%(_=>_)_,_»_,_») | 46 |
| Theorems | 0 |
| Total | 46 |
Mathlib.Notation3
Definitions
| Name | Category | Theorems |
|---|---|---|
BoundValueType 📖 | CompData | — |
DelabKey 📖 | CompData | — |
MatchState 📖 | CompData | — |
Matcher 📖 | CompOp | — |
bindersItem 📖 | CompOp | — |
expandFoldl 📖 | CompOp | — |
expandFoldr 📖 | CompOp | — |
exprToMatcher 📖 | CompOp | — |
foldAction 📖 | CompOp | — |
foldKind 📖 | CompOp | — |
getPrettyPrintOpt 📖 | CompOp | — |
identOptScoped 📖 | CompOp | — |
instInhabitedMatcher 📖 | CompOp | — |
instReprDelabKey 📖 | CompOp | — |
isType' 📖 | CompOp | — |
matchApp 📖 | CompOp | — |
matchExpr 📖 | CompOp | — |
matchFVar 📖 | CompOp | — |
matchFoldl 📖 | CompOp | — |
matchForall 📖 | CompOp | — |
matchLambda 📖 | CompOp | — |
matchScoped 📖 | CompOp | — |
matchTypeOf 📖 | CompOp | — |
matchVar 📖 | CompOp | — |
mkExprMatcher 📖 | CompOp | — |
mkFoldlMatcher 📖 | CompOp | — |
mkFoldrMatcher 📖 | CompOp | — |
mkScopedMatcher 📖 | CompOp | — |
natLitMatcher 📖 | CompOp | — |
notation3Item 📖 | CompOp | — |
prettyPrintOpt 📖 | CompOp | — |
setupLCtx 📖 | CompOp | — |
withHeadRefIfTagAppFns 📖 | CompOp | — |
«termExpand_binders%(_=>_)_,_» 📖_,_» "API Documentation") | CompOp | — |
Mathlib.Notation3.DelabKey
Definitions
| Name | Category | Theorems |
|---|---|---|
key 📖 | CompOp | — |
Mathlib.Notation3.MatchState
Definitions
| Name | Category | Theorems |
|---|---|---|
captureSubexpr 📖 | CompOp | — |
delabVar 📖 | CompOp | — |
empty 📖 | CompOp | — |
foldState 📖 | CompOp | — |
getBinders 📖 | CompOp | — |
getFoldArray 📖 | CompOp | — |
pushFold 📖 | CompOp | — |
scopeState 📖 | CompOp | — |
vars 📖 | CompOp | — |
withVar 📖 | CompOp | — |
Mathlib.Notation3.instReprDelabKey
Definitions
| Name | Category | Theorems |
|---|---|---|
repr 📖 | CompOp | — |
---