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

• 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 `Std.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.

The dynamic state of a Matcher.

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

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

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

• Mathlib.Notation3.MatchState.getFoldArray s name = Option.getD (Lean.HashMap.find? s.foldState name) #[]

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

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

Equations

• Mathlib.Notation3.MatchState.getBinders s = Option.getD s.scopeState #[]

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

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

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

Matcher for Expr.const.

Equations

• Mathlib.Notation3.matchConst c s = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr guard (Lean.Expr.isConstOf __do_lift c = true) pure s

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

Matcher for Expr.fvar. This is only used for local notation3. It checks that the user name agrees, which isn't completely accurate, but probably sufficient.

Equations

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

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

Matches raw nat lits and OfNat.ofNat expressions.

Equations

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

def Mathlib.Notation3.getExplicitArgIndices (f : Lean.Syntax) : OptionT Lean.Elab.TermElabM (Option Lean.Name × Lean.Term × Nat × Array Nat)

Given an identifier f, returns (1) the resolved constant (if it's not an fvar) (2) a Term for a matcher for the function (3) the arity (4) the positions at which the function takes an explicit argument

Equations

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

def Mathlib.Notation3.getExplicitArgIndices.collectIdxs (ty : Lean.Expr) : Lean.MetaM (Nat × Array Nat)

Equations

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

def Mathlib.Notation3.fnArgMatcher (arity : Nat) (matchf : Mathlib.Notation3.Matcher) (matchers : Array (Nat × Mathlib.Notation3.Matcher)) : Mathlib.Notation3.Matcher

A matcher that runs matchf for the function and the matchers for the associated argument indices. Fails if the function doesn't have exactly arity arguments.

Equations

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

partial def Mathlib.Notation3.mkExprMatcher (stx : Lean.Term) (boundNames : Lean.HashSet 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.

partial def Mathlib.Notation3.mkExprMatcher.processFn (boundNames : Lean.HashSet Lean.Name) (f : Lean.Term) (args : Lean.TSyntaxArray `term) : OptionT Lean.Elab.TermElabM (List Lean.Name × Lean.Term)

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 `Std.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 : Lean.HashSet Lean.Name) : OptionT Lean.Elab.TermElabM (List Lean.Name × Lean.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 : Lean.HashSet 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 : Lean.HashSet 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

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

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

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.«command___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.