The notation3 macro, simulating Lean 3's notation.

Syntaxes supporting notation3

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.

def Mathlib.Notation3.expandFoldl : Lean.ParserDescr

Equations

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

def Mathlib.Notation3.expandFoldr : Lean.ParserDescr

Equations

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

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.

def Mathlib.Notation3.bindersItem : Lean.ParserDescr

notation3 argument matching extBinders.

Equations

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

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.

def Mathlib.Notation3.identOptScoped : Lean.ParserDescr

notation3 argument binding a name.

Equations

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

def Mathlib.Notation3.notation3Item : Lean.ParserDescr

notation3 argument.

Equations

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

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).

structure Mathlib.Notation3.MatchState : Type

The dynamic state of a Matcher.

• vars : Lean.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 : Lean.HashMap Lean.Name (Array Lean.Term)

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

def Mathlib.Notation3.Matcher : Type

A matcher is a delaboration function that transforms MatchStates.

Equations

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

def Mathlib.Notation3.MatchState.empty : Mathlib.Notation3.MatchState

The initial state.

Equations

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

def Mathlib.Notation3.MatchState.withVar {α : Type} (s : Mathlib.Notation3.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.find? name with | some (se, lctx, linsts) => Lean.Meta.withLCtx lctx linsts (withTheReader Lean.SubExpr (fun (x : Lean.SubExpr) => se) m) | x => failure

def Mathlib.Notation3.MatchState.delabVar (s : Mathlib.Notation3.MatchState) (name : Lean.Name) (checkNot? : optParam (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.

def Mathlib.Notation3.MatchState.captureSubexpr (s : Mathlib.Notation3.MatchState) (name : Lean.Name) : Lean.PrettyPrinter.Delaborator.DelabM Mathlib.Notation3.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.

def Mathlib.Notation3.MatchState.getFoldArray (s : Mathlib.Notation3.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.find? name).getD #[]

def Mathlib.Notation3.MatchState.getBinders (s : Mathlib.Notation3.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 #[]

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

Push a delaborated term onto a foldr/foldl array.

Equations

• s.pushFold name t = let ts := (s.getFoldArray name).push t; { vars := s.vars, scopeState := s.scopeState, foldState := s.foldState.insert name ts }

def Mathlib.Notation3.matchVar (c : Lean.Name) : Mathlib.Notation3.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.

def Mathlib.Notation3.matchExpr (p : Lean.Expr → Bool) : Mathlib.Notation3.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

def Mathlib.Notation3.matchFVar (userName : Lean.Name) (matchTy : Mathlib.Notation3.Matcher) : Mathlib.Notation3.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.

def Mathlib.Notation3.matchTypeOf (matchTy : Mathlib.Notation3.Matcher) : Mathlib.Notation3.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)

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

Matches raw nat lits.

Equations

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

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

Matches applications.

Equations

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

def Mathlib.Notation3.matchForall (matchDom : Mathlib.Notation3.Matcher) (matchBody : Lean.Expr → Mathlib.Notation3.Matcher) : Mathlib.Notation3.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.

def Mathlib.Notation3.matchLambda (matchDom : Mathlib.Notation3.Matcher) (matchBody : Lean.Expr → Mathlib.Notation3.Matcher) : Mathlib.Notation3.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.

def Mathlib.Notation3.setupLCtx (lctx : Lean.LocalContext) (boundNames : Array Lean.Name) : Lean.MetaM (Lean.LocalContext × Lean.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.

partial def Mathlib.Notation3.exprToMatcher (boundFVars : Lean.HashMap Lean.FVarId Lean.Name) (localFVars : Lean.HashMap Lean.FVarId Lean.Term) (e : Lean.Expr) : OptionT Lean.Elab.TermElabM (List Lean.Name × 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.

def Mathlib.Notation3.mkExprMatcher (stx : Lean.Term) (boundNames : Array Lean.Name) : OptionT Lean.Elab.TermElabM (List Lean.Name × 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.

def Mathlib.Notation3.matchScoped (lit : Lean.Name) (scopeId : Lean.Name) (smatcher : Mathlib.Notation3.Matcher) : Mathlib.Notation3.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 #[]

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

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

def Mathlib.Notation3.mkScopedMatcher (lit : Lean.Name) (scopeId : Lean.Name) (scopedTerm : Lean.Term) (boundNames : Array Lean.Name) : OptionT Lean.Elab.TermElabM (List Lean.Name × 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.

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

Matcher for expressions produced by foldl.

def Mathlib.Notation3.mkFoldlMatcher (lit : Lean.Name) (x : Lean.Name) (y : Lean.Name) (scopedTerm : Lean.Term) (init : Lean.Term) (boundNames : Array Lean.Name) : OptionT Lean.Elab.TermElabM (List Lean.Name × 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.

def Mathlib.Notation3.mkFoldrMatcher (lit : Lean.Name) (x : Lean.Name) (y : Lean.Name) (scopedTerm : Lean.Term) (init : Lean.Term) (boundNames : Array Lean.Name) : OptionT Lean.Elab.TermElabM (List Lean.Name × 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.

The notation3 command

def Mathlib.Notation3.mkNameFromSyntax (name? : Option (Lean.TSyntax `Lean.Parser.Command.namedName)) (syntaxArgs : Array (Lean.TSyntax `stx)) (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) : Lean.Elab.Command.CommandElabM Lean.Name

Create a name that we can use for the syntax definition, using the algorithm from notation.

Equations

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

inductive Mathlib.Notation3.BoundValueType : Type

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

• normal: Mathlib.Notation3.BoundValueType

  A normal variable, delaborate its expression.

• foldl: Mathlib.Notation3.BoundValueType

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

• foldr: Mathlib.Notation3.BoundValueType

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

def Mathlib.Notation3.prettyPrintOpt : Lean.ParserDescr

Equations

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

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.

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.

scoped[ns] support