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

def Mathlib.Notation3.expandFoldl : Lean.ParserDescr

def Mathlib.Notation3.expandFoldr : Lean.ParserDescr

def Mathlib.Notation3.foldKind : Lean.ParserDescr

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

def Mathlib.Notation3.bindersItem : Lean.ParserDescr

notation3 argument matching extBinders.

def Mathlib.Notation3.foldAction : Lean.ParserDescr

notation3 argument simulating a Lean 3 fold notation.

def Mathlib.Notation3.identOptScoped : Lean.ParserDescr

notation3 argument binding a name.

def Mathlib.Notation3.notation3Item : Lean.ParserDescr

notation3 argument.

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

@[implicit_reducible]

instance Mathlib.Notation3.instInhabitedMatcher : Inhabited Matcher

def Mathlib.Notation3.MatchState.empty : MatchState

The initial state.

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.

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

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.

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.

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.

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

Push a delaborated term onto a foldr/foldl array.

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.

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

Matcher for an expression satisfying a given predicate.

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.

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

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

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

Matches raw Nat literals.

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

Matches applications.

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.

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

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

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

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

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

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 : ℕ) : DelabKey

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

• other (key : Lean.Name) : DelabKey

def Mathlib.Notation3.instReprDelabKey.repr : DelabKey → ℕ → Std.Format

@[implicit_reducible]

instance Mathlib.Notation3.instReprDelabKey : Repr DelabKey

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

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

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.

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.

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.

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)

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

Matcher for expressions produced by foldl.

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)

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)

The notation3 command

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

def Mathlib.Notation3.prettyPrintOpt : Lean.ParserDescr

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

Interpret a prettyPrintOpt. The default value is true.

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.

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.

scoped[ns] support