doc-next-gen

Init.NotationExtra

Module docstring

{}

Lean.unbracketedExplicitBinders definition
: Lean.ParserDescr✝
Full source 
syntax unbracketedExplicitBinders := (ppSpace binderIdent)+ (" : " term)?
Unbracketed explicit binders syntax
Informal description
The syntax definition `unbracketedExplicitBinders` specifies how to parse unbracketed explicit binders in Lean, which are space-separated binder identifiers optionally followed by a type annotation. This is used for declaring variables or parameters without surrounding brackets.
Lean.bracketedExplicitBinders definition
: Lean.ParserDescr✝
Full source 
syntax bracketedExplicitBinders   := "(" withoutPosition((binderIdent ppSpace)+ ": " term) ")"
Syntax for parenthesized explicit binders
Informal description
The syntax definition `bracketedExplicitBinders` describes a parser for explicit binders in Lean that are enclosed in parentheses. It matches patterns of the form `(ident1 ident2 ... : type)` where one or more binder identifiers are followed by a colon and a type term.
Lean.explicitBinders definition
: Lean.ParserDescr✝
Full source 
syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unbracketedExplicitBinders
Syntax for explicit binders
Informal description
The syntax definition `explicitBinders` describes a parser for explicit binders in Lean, which can be either a sequence of space-separated parenthesized binders (using `bracketedExplicitBinders`) or an unbracketed binder (using `unbracketedExplicitBinders`). This allows for flexible declaration of variables or parameters in Lean syntax.
Lean.expandExplicitBindersAux definition
(combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax
Full source 
def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
  let rec loop (i : Nat) (h : i ≤ idents.size) (acc : Syntax) := do
    match i with
    | 0   => pure acc
    | i + 1 =>
      let ident := idents[i][0]
      let acc ← match ident.isIdent, type? with
        | true,  none      => `($combinator fun $ident => $acc)
        | true,  some type => `($combinator fun $ident : $type => $acc)
        | false, none      => `($combinator fun _ => $acc)
        | false, some type => `($combinator fun _ : $type => $acc)
      loop i (Nat.le_of_succ_le h) acc
  loop idents.size (by simp) body
Auxiliary function for expanding explicit binders with a combinator
Informal description
The auxiliary function `expandExplicitBindersAux` takes a combinator syntax, an array of identifiers, an optional type syntax, and a body syntax, and recursively applies the combinator to each identifier (with its type if provided) to build a nested syntax tree. For each identifier in the array, it constructs a lambda expression with the identifier and its type (if available), applying the combinator at each step. The recursion starts from the end of the array and works backwards, accumulating the result into the body syntax.
Lean.expandBrackedBindersAux definition
(combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax
Full source 
def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
  let rec loop (i : Nat) (h : i ≤ binders.size) (acc : Syntax) := do
    match i with
    | 0   => pure acc
    | i+1 =>
      let idents := binders[i][1].getArgs
      let type   := binders[i][3]
      loop i (Nat.le_of_succ_le h) (← expandExplicitBindersAux combinator idents (some type) acc)
  loop binders.size (by simp) body
Auxiliary function for expanding bracketed binders with a combinator
Informal description
The auxiliary function `expandBrackedBindersAux` takes a combinator syntax, an array of binder syntax elements, and a body syntax, and recursively processes each binder to build a nested syntax tree. For each binder in the array, it extracts the identifiers and their type (if provided), and applies the combinator to construct a lambda expression with the identifier and type, accumulating the result into the body syntax. The recursion starts from the end of the array and works backwards.
Lean.expandExplicitBinders definition
(combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax
Full source 
def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
  let combinator := mkCIdentFrom (← getRef) combinatorDeclName
  let explicitBinders := explicitBinders[0]
  if explicitBinders.getKind == ``Lean.unbracketedExplicitBinders then
    let idents   := explicitBinders[0].getArgs
    let type? := if explicitBinders[1].isNone then none else some explicitBinders[1][1]
    expandExplicitBindersAux combinator idents type? body
  else if explicitBinders.getArgs.all (·.getKind == ``Lean.bracketedExplicitBinders) then
    expandBrackedBindersAux combinator explicitBinders.getArgs body
  else
    Macro.throwError "unexpected explicit binder"
Expansion of explicit binders with a combinator
Informal description
The function `expandExplicitBinders` takes a combinator declaration name, a syntax element representing explicit binders, and a body syntax, and processes them to construct a nested syntax tree. It first creates a combinator identifier from the given declaration name, then checks the kind of the explicit binders. If the binders are unbracketed, it extracts the identifiers and their optional type, and uses the auxiliary function `expandExplicitBindersAux` to recursively process them. If the binders are bracketed, it uses the auxiliary function `expandBrackedBindersAux` to process them. If the binders are neither, it throws an error.
Lean.expandBrackedBinders definition
(combinatorDeclName : Name) (bracketedExplicitBinders : Syntax) (body : Syntax) : MacroM Syntax
Full source 
def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
  let combinator := mkCIdentFrom (← getRef) combinatorDeclName
  expandBrackedBindersAux combinator #[bracketedExplicitBinders] body
Expansion of bracketed binders with a combinator
Informal description
The function `expandBrackedBinders` takes a combinator declaration name, a syntax element representing bracketed explicit binders, and a body syntax, and processes them to construct a nested syntax tree. It first creates a combinator identifier from the given declaration name, then uses the auxiliary function `expandBrackedBindersAux` to recursively process the binders and build the resulting syntax tree with the provided body.
Lean.unifConstraint definition
: Lean.ParserDescr✝
Full source 
syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
Unification constraint syntax
Informal description
The syntax definition `unifConstraint` represents a unification constraint in Lean, which is written in the form `term₁ =?= term₂` or `term₁ ≟ term₂`, where `term₁` and `term₂` are arbitrary terms that need to be unified.
Lean.unifConstraintElem definition
: Lean.ParserDescr✝
Full source 
syntax unifConstraintElem := colGe unifConstraint ", "?
Unification constraint element syntax
Informal description
The syntax element representing a single unification constraint in Lean, which is written as `term₁ =?= term₂` or `term₁ ≟ term₂`, optionally followed by a comma. This is used to specify that two terms need to be unified.
Lean.command__Unif_hint____Where_|_-⊢_ definition
: Lean.ParserDescr✝
Full source 
syntaxsyntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
Unification hint command syntax
Informal description
The syntax definition for the `unif_hint` command in Lean, which allows specifying unification hints. The command takes optional documentation comments and attributes, followed by an optional identifier and binders, then a list of unification constraints after the keyword "where". The constraints are written in the form `term₁ =?= term₂` or `term₁ ≟ term₂`, optionally followed by a comma. The command concludes with either a pattern separator `|` followed by a constraint or the turnstile symbol `⊢` followed by a constraint.
termExists_,_ definition
: Lean.ParserDescr✝
Full source 
macromacro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
Existential quantifier syntax macro (alternative form)
Informal description
The syntax macro `exists` followed by explicit binders `xs` and a term `b` expands to the existential quantifier `Exists` applied to the binders `xs` and the term `b`. This provides an alternative syntax for writing existential statements in Lean.
termΣ'_,_ definition
: Lean.ParserDescr✝
Full source 
macromacro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``PSigma xs b
Dependent product type with explicit binders (PSigma notation)
Informal description
The syntax macro `termΣ'_,_` defines a parser for the notation `Σ' (x y ... : T), b`, which expands to `PSigma (fun (x y ... : T) => b)` using the `expandExplicitBinders` function. This represents a dependent product type with explicit binders.
Lean.calcFirstStep definition
: Lean.ParserDescr✝
Full source 
syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
First step parser for calculation blocks
Informal description
The parser definition for the first step in a Lean calculation block, which consists of an indented term optionally followed by a justification after `:=`.
Lean.calcStep definition
: Lean.ParserDescr✝
Full source 
syntax calcStep := ppIndent(colGe term " := " term)
Calculation step syntax in Lean
Informal description
The syntax definition for a single step in a Lean calculation proof, where each step consists of a term followed by `:=` and another term, with proper indentation and column alignment.
Lean.calc definition
: Lean.ParserDescr✝
Full source 
/-- Step-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer:
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
-/
syntax (name := calc) "calc" calcSteps : term
Step-wise reasoning syntax (`calc`)
Informal description
The `calc` syntax allows step-wise reasoning over transitive relations. It can be used to prove statements like $a = z$ through a sequence of intermediate steps: ``` calc a = b := pab b = c := pbc ... y = z := pyz ``` where each step is justified by a proof. The relation `=` can be replaced with any transitive relation. Subsequent left-hand sides can be replaced with `_` for brevity: ``` calc a = b := pab _ = c := pbc ... _ = z := pyz ``` This syntax works as a term, tactic, or in conversion mode.
Lean.calcTactic definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc «calc»]
syntax (name := calcTactic) "calc" calcSteps : tactic
Calculation tactic syntax in Lean
Informal description
The syntax definition for the `calc` tactic in Lean, which allows writing calculation proofs with a sequence of steps. The first step is parsed using `calcFirstStep` and subsequent steps are parsed using `calcStep`, with proper line breaks and indentation.
Lean.convCalc_ definition
: Lean.ParserDescr✝
Full source 
macromacro tk:"calc" steps:calcSteps : conv =>
  `(conv| tactic => calc%$tk $steps)
Calculation tactic in conversion mode
Informal description
The syntax definition for the `calc` tactic in conversion mode in Lean, which allows writing calculation proofs with a sequence of steps during conversion. The first step is parsed using `calcFirstStep` and subsequent steps are parsed using `calcStep`, with proper line breaks and indentation.
unexpandUnit definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
  | `($(_)) => `(())
Unit notation unexpander
Informal description
The `unexpandUnit` function is a syntax unexpander that transforms the unit notation `()` back to its canonical form during pretty printing.
unexpandListNil definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
  | `($(_)) => `([])
Empty list notation unexpander
Informal description
The unexpander `unexpandListNil` transforms the empty list notation `[]` back to its syntactic form during pretty-printing.
unexpandListCons definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
  | `($(_) $x $tail) =>
    match tail with
    | `([])      => `([$x])
    | `([$xs,*]) => `([$x, $xs,*])
    | `(⋯)       => `([$x, $tail]) -- Unexpands to `[x, y, z, ⋯]` for `⋯ : List α`
    | _          => throw ()
  | _ => throw ()
List cons unexpander
Informal description
The unexpander function for list cons notation, which transforms expressions of the form `($x $tail)` into list notation `[$x, ...]`, handling various cases for the tail of the list.
unexpandProdMk definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
  | `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
  | `($(_) $x $y)          => `(($x, $y))
  | _                      => throw ()
Product constructor unexpander
Informal description
The unexpander for product constructor notation, which transforms expressions of the form `Prod.mk x y` into the pair notation `(x, y)` and `Prod.mk x (y, ys, ...)` into the tuple notation `(x, y, ys, ...)`.
unexpandIte definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
  | `($(_) $c $t $e) => `(if $c then $t else $e)
  | _                => throw ()
Unexpander for if-then-else expressions
Informal description
The function `unexpandIte` is a pretty-printer unexpander that transforms the syntax of an `if-then-else` expression back into its more readable form. Specifically, it matches patterns of the form `($(_) $c $t $e)` and converts them into `if $c then $t else $e`, where `$c` is the condition, `$t` is the "then" branch, and `$e` is the "else" branch. If the input does not match this pattern, the function throws an error.
unexpandEqNDRec definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
  | `($(_) $m $h) => `($h ▸ $m)
  | _             => throw ()
Unexpander for dependent equality elimination
Informal description
The unexpander `unexpandEqNDRec` transforms expressions of the form `(m h)` into `(h ▸ m)`, where `▸` represents the dependent elimination rule for equality (also known as "transport" or "substitution"). This is used for pretty-printing purposes in the Lean proof assistant.
unexpandExists definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
  | `($(_) fun $x:ident => $b)                     => `(∃ $x:ident, $b)
  | `($(_) fun ($x:ident : $t) => $b)              => `(∃ ($x:ident : $t), $b)
  | _                                              => throw ()
Existential quantifier unexpander
Informal description
The unexpander for the existential quantifier `∃` in Lean's pretty printer. It handles patterns of the form `∃ x, p`, `∃ x : T, p`, and `∃ x₁ ... xₙ, p`, transforming them from their functional notation back to the standard existential quantifier syntax.
unexpandSubtype definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Subtype] def unexpandSubtype : Lean.PrettyPrinter.Unexpander
  | `($(_) fun ($x:ident : $type) => $p)  => `({ $x : $type // $p })
  | `($(_) fun $x:ident => $p)            => `({ $x // $p })
  | _                                     => throw ()
Subtype notation unexpander
Informal description
The unexpander for subtype notation, which transforms expressions of the form `fun (x : type) => p` or `fun x => p` into the subtype notation `{x : type // p}` or `{x // p}` respectively. This is used in the Lean pretty printer to display subtypes in a more readable format.
unexpandGetElem! definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander getElem!] def unexpandGetElem! : Lean.PrettyPrinter.Unexpander
  | `($_ $array $index) => `($array[$index]!)
  | _ => throw ()
Unexpander for `getElem!` array notation
Informal description
The unexpander function for transforming syntax trees involving the `getElem!` operation in the Lean pretty printer, converting expressions of the form `getElem! array index` into the more familiar array indexing notation `array[index]!`.
unexpandArrayEmpty definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
  | _ => `(#[])
Empty array notation unexpander
Informal description
The unexpander function `unexpandArrayEmpty` translates the syntax for an empty array in Lean to the notation `#[]`.
unexpandMkArray0 definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.mkArray0] def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
  | _ => `(#[])
Unexpander for empty array syntax
Informal description
The unexpander function for the `MkArray0` syntax, which transforms it back to the empty array notation `#[]`.
unexpandMkArray3 definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.mkArray3] def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander
  | `($(_) $a1 $a2 $a3) => `(#[$a1, $a2, $a3])
  | _ => throw ()
Unexpander for three-element array syntax
Informal description
The unexpander function `unexpandMkArray3` transforms the syntax `($(_) $a1 $a2 $a3)` into `#[$a1, $a2, $a3]`, which represents an array with three elements. If the input doesn't match this pattern, it throws an error.
unexpandMkArray5 definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.mkArray5] def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander
  | `($(_) $a1 $a2 $a3 $a4 $a5) => `(#[$a1, $a2, $a3, $a4, $a5])
  | _ => throw ()
Unexpander for 5-element array constructor
Informal description
The unexpander definition for `mkArray5` syntax, which transforms the application `mkArray5 a1 a2 a3 a4 a5` into the array literal notation `#[a1, a2, a3, a4, a5]`. This is used for pretty-printing purposes in the Lean proof assistant.
unexpandMkArray6 definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.mkArray6] def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander
  | `($(_) $a1 $a2 $a3 $a4 $a5 $a6) => `(#[$a1, $a2, $a3, $a4, $a5, $a6])
  | _ => throw ()
Unexpander for 6-element array constructor
Informal description
The unexpander definition for `mkArray6` syntax, which transforms the application `mkArray6 a1 a2 a3 a4 a5 a6` into the array literal notation `#[a1, a2, a3, a4, a5, a6]`. This is used for pretty-printing purposes in the Lean proof assistant.
unexpandMkArray7 definition
: Lean.PrettyPrinter.Unexpander
Full source 
@[app_unexpander Array.mkArray7] def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander
  | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7])
  | _ => throw ()
Unexpander for 7-element array constructor
Informal description
The unexpander definition for `mkArray7` syntax, which transforms the application `mkArray7 a1 a2 a3 a4 a5 a6 a7` into the array literal notation `#[a1, a2, a3, a4, a5, a6, a7]`. This is used for pretty-printing purposes in the Lean proof assistant.
tacticFunext___ definition
: Lean.ParserDescr✝
Full source 
/--
Apply function extensionality and introduce new hypotheses.
The tactic `funext` will keep applying the `funext` lemma until the goal target is not reducible to
```
  |-  ((fun x => ...) = (fun x => ...))
```
The variant `funext h₁ ... hₙ` applies `funext` `n` times, and uses the given identifiers to name the new hypotheses.
Patterns can be used like in the `intro` tactic. Example, given a goal
```
  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))
```
`funext (a, b)` applies `funext` once and performs pattern matching on the newly introduced pair.
-/
syntax "funext" (ppSpace colGt term:max)* : tactic
Function extensionality tactic
Informal description
The tactic `funext` applies function extensionality repeatedly to a goal of the form `(fun x => ...) = (fun x => ...)`, introducing new hypotheses for each application. It can also be used with specific identifiers `h₁ ... hₙ` to name the new hypotheses, and supports pattern matching similar to the `intro` tactic.
Lean.Parser.Command.classAbbrev definition
: Lean.ParserDescr✝
Full source 
/--
  Expands
  ```
  class abbrev C <params> := D_1, ..., D_n
  ```
  into
  ```
  class C <params> extends D_1, ..., D_n
  attribute [instance] C.mk
  ```
-/
syntax (name := Lean.Parser.Command.classAbbrev)
  declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
  ":=" withPosition(group(colGe term ","?)*) : command
Class abbreviation syntax expansion
Informal description
The syntax `class abbrev C := D_1, ..., D_n` is expanded into a class definition `class C extends D_1, ..., D_n` with an automatically generated instance attribute `[instance] C.mk`.
Lean.cdotTk definition
: Lean.ParserDescr✝
Full source 
syntax cdotTk := patternIgnore("· " <|> ". ")
Middle dot or period syntax token
Informal description
The syntax definition `cdotTk` recognizes either the Unicode middle dot symbol "·" followed by a space or a period "." followed by a space in Lean's parser.
Lean.solveTactic definition
: Lean.ParserDescr✝
Full source 
/--
  Similar to `first`, but succeeds only if one the given tactics solves the current goal.
-/
syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
Solve tactic (conditional first)
Informal description
The `solve` tactic attempts to apply one of the given tactics to solve the current goal, succeeding only if one of them completely solves the goal (unlike `first` which may succeed even if the goal isn't fully solved). The syntax requires each tactic alternative to be preceded by `| ` and properly indented.
Lean.term_Matches_| definition
: Lean.TrailingParserDescr✝
Full source 
macromacro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
  `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
Pattern matching macro
Informal description
The macro `e matches p₁ | p₂ | ... | pₙ` checks whether the term `e` matches any of the patterns `p₁`, `p₂`, ..., `pₙ`, returning a boolean value. It expands to a match expression that returns `true` if `e` matches any pattern and `false` otherwise.
Lean.singletonUnexpander definition
: Lean.PrettyPrinter.Unexpander
Full source 
/-- Unexpander for the `{ x }` notation. -/
@[app_unexpander singleton]
def singletonUnexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $a) => `({ $a:term })
  | _ => throw ()
Unexpander for singleton set notation
Informal description
The unexpander for the singleton set notation `{x}`, which transforms the internal representation `singleton x` back to the surface syntax `{x}`. This handles the case where the set contains exactly one element.