def Lean.«termMacro.trace[_]_» : Lean.ParserDescr

Equations

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

def Lean.unbracketedExplicitBinders : Lean.ParserDescr

Equations

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

def Lean.bracketedExplicitBinders : Lean.ParserDescr

Equations

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

def Lean.explicitBinders : Lean.ParserDescr

Equations

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

def Lean.expandExplicitBindersAux (combinator : Lean.Syntax) (idents : Array Lean.Syntax) (type? : Option Lean.Syntax) (body : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

• Lean.expandExplicitBindersAux combinator idents type? body = Lean.expandExplicitBindersAux.loop combinator idents type? (Array.size idents) body

def Lean.expandExplicitBindersAux.loop (combinator : Lean.Syntax) (idents : Array Lean.Syntax) (type? : Option Lean.Syntax) (i : Nat) (acc : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

• One or more equations did not get rendered due to their size.
• Lean.expandExplicitBindersAux.loop combinator idents type? 0 acc = pure acc

def Lean.expandBrackedBindersAux (combinator : Lean.Syntax) (binders : Array Lean.Syntax) (body : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

• Lean.expandBrackedBindersAux combinator binders body = Lean.expandBrackedBindersAux.loop combinator binders (Array.size binders) body

def Lean.expandBrackedBindersAux.loop (combinator : Lean.Syntax) (binders : Array Lean.Syntax) (i : Nat) (acc : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

• One or more equations did not get rendered due to their size.
• Lean.expandBrackedBindersAux.loop combinator binders 0 acc = pure acc

def Lean.expandExplicitBinders (combinatorDeclName : Lake.Name) (explicitBinders : Lean.Syntax) (body : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

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

def Lean.expandBrackedBinders (combinatorDeclName : Lake.Name) (bracketedExplicitBinders : Lean.Syntax) (body : Lean.Syntax) : Lean.MacroM Lean.Syntax

Equations

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

def Lean.unifConstraint : Lean.ParserDescr

Equations

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

def Lean.unifConstraintElem : Lean.ParserDescr

Equations

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

def Lean.«command__Unif_hint____Where_|_-⊢_» : Lean.ParserDescr

Equations

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

def «term∃_,_» : Lean.ParserDescr

Equations

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

def «termExists_,_» : Lean.ParserDescr

Equations

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

def «termΣ_,_» : Lean.ParserDescr

Equations

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

def «termΣ'_,_» : Lean.ParserDescr

Equations

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

def «term_×__1» : Lean.ParserDescr

Equations

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

def «term_×'_» : Lean.ParserDescr

Equations

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

def calcFirstStep : Lean.ParserDescr

Equations

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

def calcStep : Lean.ParserDescr

Equations

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

def calcSteps : Lean.ParserDescr

Equations

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

def calc : Lean.ParserDescr

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 has term mode and tactic mode variants. This is the term mode variant.

See Theorem Proving in Lean 4 for more information.

Equations

• calc = Lean.ParserDescr.node `calc 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "calc") calcSteps)

def calcTactic : Lean.ParserDescr

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:

calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz

calc has term mode and tactic mode variants. This is the tactic mode variant, which supports an additional feature: it works even if the goal is a = z' for some other z'; in this case it will not close the goal but will instead leave a subgoal proving z = z'.

See Theorem Proving in Lean 4 for more information.

Equations

• calcTactic = Lean.ParserDescr.node `calcTactic 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "calc" false) calcSteps)

def «term⋯» : Lean.ParserDescr

Denotes a term that was omitted by the pretty printer. This is only used for pretty printing, and it cannot be elaborated. The presence of ⋯ is controlled by the pp.deepTerms and pp.deepTerms.threshold options.

Equations

• «term⋯» = Lean.ParserDescr.node `term⋯ 1024 (Lean.ParserDescr.symbol "⋯")

def unexpandUnit : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandListNil : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandListCons : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandListToArray : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandProdMk : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandIte : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandSorryAx : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandEqRec : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandExists : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandSigma : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandPSigma : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandSubtype : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandTSyntax : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandTSyntaxArray : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandTSepArray : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandGetElem : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandGetElem! : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandGetElem? : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander

Equations

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

def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander

Equations

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

def tacticFunext___ : Lean.ParserDescr

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.

Equations

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

def Lean.Parser.Command.classAbbrev : Lean.ParserDescr

Expands

class abbrev C <params> := D_1, ..., D_n

into

class C <params> extends D_1, ..., D_n
attribute [instance] C.mk

Equations

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

def cdotTk : Lean.ParserDescr

Equations

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

def cdot : Lean.ParserDescr

· tac focuses on the main goal and tries to solve it using tac, or else fails.

Equations

• cdot = Lean.ParserDescr.node `cdot 1022 (Lean.ParserDescr.binary `andthen cdotTk (Lean.ParserDescr.const `tacticSeqIndentGt))

def solve : Lean.ParserDescr

Similar to first, but succeeds only if one the given tactics solves the current goal.

Equations

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

repeat and while notation

inductive Lean.Loop : Type

• mk: Lean.Loop

@[inline]

def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] : Lean.Loop → β → (Unit → β → m (ForInStep β)) → m β

Equations

• Lean.Loop.forIn x init f = Lean.Loop.forIn.loop f init

@[specialize #[]]

partial def Lean.Loop.forIn.loop {β : Type u} {m : Type u → Type v} [Monad m] (f : Unit → β → m (ForInStep β)) (b : β) : m β

instance Lean.instForInLoopUnit {m : Type u_1 → Type u_2} : ForIn m Lean.Loop Unit

Equations

• Lean.instForInLoopUnit = { forIn := fun {β : Type u_1} [Monad m] => Lean.Loop.forIn }

def Lean.doElemRepeat_ : Lean.ParserDescr

Equations

• Lean.doElemRepeat_ = Lean.ParserDescr.node `Lean.doElemRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq))

def Lean.«doElemWhile_:_Do_» : Lean.ParserDescr

Equations

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

def Lean.doElemWhile_Do_ : Lean.ParserDescr

Equations

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

def Lean.doElemRepeat__Until_ : Lean.ParserDescr

Equations

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

def Lean.«term_Matches_|» : Lean.TrailingParserDescr

Equations

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