# The notation3 macro, simulating Lean 3's notation. #

### Syntaxes supporting `notation3` #

source
def Mathlib.Notation3.«termExpand_binders%(_=>_)_,_» :
Lean.ParserDescr

Expands binders into nested combinators. For example, the familiar exists is given by: `expand_binders% (p => Exists p) x y : Nat, x < y` which expands to the same expression as `∃ x y : Nat, x < y`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.expandFoldl :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.expandFoldr :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.foldKind :
Lean.ParserDescr

Keywording indicating whether to use a left- or right-fold.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.bindersItem :
Lean.ParserDescr

`notation3` argument matching `extBinders`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.foldAction :
Lean.ParserDescr

`notation3` argument simulating a Lean 3 fold notation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.identOptScoped :
Lean.ParserDescr

`notation3` argument binding a name.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.notation3Item :
Lean.ParserDescr

`notation3` argument.

Equations

- One or more equations did not get rendered due to their size.

Instances For

### Expression matching #

A more complicated part of `notation3` is the delaborator generator. While `notation` relies on generating app unexpanders, we instead generate a delaborator directly so that we can control how binders are formatted (we want to be able to know the types of binders, whether a lambda is a constant function, and whether it is `Prop`-valued, which are not things we can answer once we pass to app unexpanders).

source
structure Mathlib.Notation3.MatchState :
Type

The dynamic state of a `Matcher`.

- vars : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances)

  This stores the assignments of variables to subexpressions (and their contexts) that have been found so far during the course of the matching algorithm. We store the contexts since we need to delaborate expressions after we leave scoping constructs.

- scopeState : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized))

  The binders accumulated while matching a `scoped` expression.

- foldState : Std.HashMap Lean.Name (Array Lean.Term)

  The arrays of delaborated `Term`s accumulated while matching `foldl` and `foldr` expressions. For `foldl`, the arrays are stored in reverse order.

Instances For

source
def Mathlib.Notation3.Matcher :
Type

A matcher is a delaboration function that transforms `MatchState`s.

Equations

- Mathlib.Notation3.Matcher = (Mathlib.Notation3.MatchState → Lean.PrettyPrinter.Delaborator.DelabM Mathlib.Notation3.MatchState)

Instances For

source
instance Mathlib.Notation3.instInhabitedMatcher :
Inhabited Matcher
Equations

- Mathlib.Notation3.instInhabitedMatcher = instInhabitedForallOfMonad

source
def Mathlib.Notation3.MatchState.empty :
MatchState

The initial state.

Equations

- Mathlib.Notation3.MatchState.empty = { vars := ∅, scopeState := none, foldState := ∅ }

Instances For

source
def Mathlib.Notation3.MatchState.withVar {α : Type} (s : MatchState) (name : Lean.Name) (m : Lean.PrettyPrinter.Delaborator.DelabM α) :
Lean.PrettyPrinter.Delaborator.DelabM α

Evaluate `f` with the given variable's value as the `SubExpr` and within that subexpression's saved context. Fails if the variable has no value.

Equations

- s.withVar name m = match s.vars[name]? with | some (se, lctx, linsts) => Lean.Meta.withLCtx lctx linsts (withTheReader Lean.SubExpr (fun (x : Lean.SubExpr) => se) m) | x => failure

Instances For

source
def Mathlib.Notation3.MatchState.delabVar (s : MatchState) (name : Lean.Name) (checkNot? : Option Lean.Expr := none) :
Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

Delaborate the given variable's value. Fails if the variable has no value. If `checkNot` is provided, then checks that the expression being delaborated is not the given one (this is used to prevent infinite loops).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.MatchState.captureSubexpr (s : MatchState) (name : Lean.Name) :
Lean.PrettyPrinter.Delaborator.DelabM MatchState

Assign a variable to the current `SubExpr`, capturing the local context.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.MatchState.getFoldArray (s : MatchState) (name : Lean.Name) :
Array Lean.Term

Get the accumulated array of delaborated terms for a given foldr/foldl. Returns `#[]` if nothing has been pushed yet.

Equations

- s.getFoldArray name = s.foldState[name]?.getD #[]

Instances For

source
def Mathlib.Notation3.MatchState.getBinders (s : MatchState) :
Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)

Get the accumulated array of delaborated terms for a given foldr/foldl. Returns `#[]` if nothing has been pushed yet.

Equations

- s.getBinders = s.scopeState.getD #[]

Instances For

source
def Mathlib.Notation3.MatchState.pushFold (s : MatchState) (name : Lean.Name) (t : Lean.Term) :
MatchState

Push a delaborated term onto a foldr/foldl array.

Equations

- s.pushFold name t = { vars := s.vars, scopeState := s.scopeState, foldState := s.foldState.insert name ((s.getFoldArray name).push t) }

Instances For

source
def Mathlib.Notation3.matchVar (c : Lean.Name) :
Matcher

Matcher that assigns the current `SubExpr` into the match state; if a value already exists, then it checks for equality.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.matchExpr (p : Lean.Expr → Bool) :
Matcher

Matcher for an expression satisfying a given predicate.

Equations

- Mathlib.Notation3.matchExpr p s = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr guard (p __do_lift = true) pure s

Instances For

source
def Mathlib.Notation3.matchFVar (userName : Lean.Name) (matchTy : Matcher) :
Matcher

Matcher for `Expr.fvar`. It checks that the user name agrees and that the type of the expression is matched by `matchTy`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.matchTypeOf (matchTy : Matcher) :
Matcher

Matcher that checks that the type of the expression is matched by `matchTy`.

Equations

- Mathlib.Notation3.matchTypeOf matchTy s = Lean.PrettyPrinter.Delaborator.SubExpr.withType (matchTy s)

Instances For

source
def Mathlib.Notation3.natLitMatcher (n : Nat) :
Matcher

Matches raw `Nat` literals.

Equations

- Mathlib.Notation3.natLitMatcher n s = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr guard ((__do_lift.rawNatLit? == some n) = true) pure s

Instances For

source
def Mathlib.Notation3.matchApp (matchFun matchArg : Matcher) :
Matcher

Matches applications.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.matchForall (matchDom : Matcher) (matchBody : Lean.Expr → Matcher) :
Matcher

Matches pi types. The name `n` should be unique, and `matchBody` should use `n` as the `userName` of its fvar.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.matchLambda (matchDom : Matcher) (matchBody : Lean.Expr → Matcher) :
Matcher

Matches lambdas. The `matchBody` takes the fvar introduced when visiting the body.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.setupLCtx (lctx : Lean.LocalContext) (boundNames : Array Lean.Name) :
Lean.MetaM (Lean.LocalContext × Std.HashMap Lean.FVarId Lean.Name)

Adds all the names in `boundNames` to the local context with types that are fresh metavariables. This is used for example when initializing `p` in `(scoped p => ...)` when elaborating `...`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.isType' :
Lean.Expr → Bool

Like `Expr.isType`, but uses logic that normalizes the universe level. Mirrors the core `Sort` delaborator logic.

Equations

- Mathlib.Notation3.isType' (Lean.Expr.sort u) = u.dec.isSome
- Mathlib.Notation3.isType' x✝ = false

Instances For

source
inductive Mathlib.Notation3.DelabKey :
Type

Represents a key to use when registering the `delab` attribute for a delaborator. We use this to handle overapplication.

- app (const : Option Lean.Name) (arity : Nat) : DelabKey

  The key `app.const` or `app` with a specific arity.

- other (key : Lean.Name) : DelabKey

Instances For

source
instance Mathlib.Notation3.instReprDelabKey :
Repr DelabKey
Equations

- Mathlib.Notation3.instReprDelabKey = { reprPrec := Mathlib.Notation3.instReprDelabKey.repr }

source
def Mathlib.Notation3.instReprDelabKey.repr :
DelabKey → Nat → Std.Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.DelabKey.key :
DelabKey → Lean.Name

Turns the `DelabKey` into a key that the `delab` attribute accepts.

Equations

- (Mathlib.Notation3.DelabKey.app none arity).key = `app
- (Mathlib.Notation3.DelabKey.app (some n) arity).key = `app ++ n
- (Mathlib.Notation3.DelabKey.other key).key = key

Instances For

source
partial def Mathlib.Notation3.exprToMatcher (boundFVars : Std.HashMap Lean.FVarId Lean.Name) (localFVars : Std.HashMap Lean.FVarId Lean.Term) (e : Lean.Expr) :
OptionT Lean.Elab.TermElabM (List DelabKey × Lean.Term)

Given an expression, generate a matcher for it. The `boundFVars` hash map records which state variables certain fvars correspond to. The `localFVars` hash map records which local variable the matcher should use for an exact expression match.

If it succeeds generating a matcher, returns

1. a list of keys that should be used for the `delab` attribute when defining the elaborator
2. a `Term` that represents a `Matcher` for the given expression `e`.

source
def Mathlib.Notation3.mkExprMatcher (stx : Lean.Term) (boundNames : Array Lean.Name) :
OptionT Lean.Elab.TermElabM (List DelabKey × Lean.Term)

Returns a `Term` that represents a `Matcher` for the given pattern `stx`. The `boundNames` set determines which identifiers are variables in the pattern. Fails in the `OptionT` sense if it comes across something it's unable to handle.

Also returns constant names that could serve as a key for a delaborator. For example, if it's for a function `f`, then `app.f`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.matchScoped (lit scopeId : Lean.Name) (smatcher : Matcher) :
Matcher

Matcher for processing `scoped` syntax. Assumes the expression to be matched against is in the `lit` variable.

Runs `smatcher`, extracts the resulting `scopeId` variable, processes this value (which must be a lambda) to produce a binder, and loops.

Equations

- Mathlib.Notation3.matchScoped lit scopeId smatcher = Mathlib.Notation3.matchScoped.go lit scopeId smatcher #[]

Instances For

source
partial def Mathlib.Notation3.matchScoped.go (lit scopeId : Lean.Name) (smatcher : Matcher) (binders : Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)) :
MatchState → Lean.PrettyPrinter.Delaborator.DelabM MatchState

Variant of `matchScoped` after some number of `binders` have already been captured.

source
def Mathlib.Notation3.mkScopedMatcher (lit scopeId : Lean.Name) (scopedTerm : Lean.Term) (boundNames : Array Lean.Name) :
OptionT Lean.Elab.TermElabM (List DelabKey × Lean.Term)

Create a `Term` that represents a matcher for `scoped` notation. Fails in the `OptionT` sense if a matcher couldn't be constructed. Also returns a delaborator key like in `mkExprMatcher`. Reminder: `$lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Mathlib.Notation3.matchFoldl (lit x y : Lean.Name) (smatcher sinit : Matcher) :
Matcher

Matcher for expressions produced by `foldl`.

source
def Mathlib.Notation3.mkFoldlMatcher (lit x y : Lean.Name) (scopedTerm init : Lean.Term) (boundNames : Array Lean.Name) :
OptionT Lean.Elab.TermElabM (List DelabKey × Lean.Term)

Create a `Term` that represents a matcher for `foldl` notation. Reminder: `( lit ","* => foldl (x y => scopedTerm) init)`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.mkFoldrMatcher (lit x y : Lean.Name) (scopedTerm init : Lean.Term) (boundNames : Array Lean.Name) :
OptionT Lean.Elab.TermElabM (List DelabKey × Lean.Term)

Create a `Term` that represents a matcher for `foldr` notation. Reminder: `( lit ","* => foldr (x y => scopedTerm) init)`

Equations

- One or more equations did not get rendered due to their size.

Instances For

### The `notation3` command #

source
inductive Mathlib.Notation3.BoundValueType :
Type

Used when processing different kinds of variables when building the final delaborator.

- normal : BoundValueType

  A normal variable, delaborate its expression.

- foldl : BoundValueType

  A fold variable, use the fold state (but reverse the array).

- foldr : BoundValueType

  A fold variable, use the fold state (do not reverse the array).

Instances For

source
def Mathlib.Notation3.prettyPrintOpt :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.getPrettyPrintOpt (opt? : Option (Lean.TSyntax `Mathlib.Notation3.prettyPrintOpt)) :
Bool

Interpret a `prettyPrintOpt`. The default value is `true`.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Notation3.getPrettyPrintOpt opt? = true

Instances For

source
def Mathlib.Notation3.withHeadRefIfTagAppFns (d : Lean.PrettyPrinter.Delaborator.Delab) :
Lean.PrettyPrinter.Delaborator.Delab

If `pp.tagAppFns` is true and the head of the current expression is a constant, then delaborates the head and uses it for the ref. This causes tokens inside the syntax to refer to this constant. A consequence is that docgen will linkify the tokens.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Notation3.notation3 :
Lean.ParserDescr

`notation3` declares notation using Lean-3-style syntax.

Examples:

    notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => r
    notation3 "MyList[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x

By default notation is unable to mention any variables defined using `variable`, but `local notation3` is able to use such local variables.

Use `notation3 (prettyPrint := false)` to keep the command from generating a pretty printer for the notation.

This command can be used in mathlib4 but it has an uncertain future and was created primarily for backward compatibility.

Equations

- One or more equations did not get rendered due to their size.

Instances For

`scoped[ns]` support