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

def Lean.unbracketedExplicitBinders : Lean.ParserDescr

def Lean.bracketedExplicitBinders : Lean.ParserDescr

def Lean.explicitBinders : Lean.ParserDescr

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

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

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

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

def Lean.unifConstraint : Lean.ParserDescr

def Lean.unifConstraintElem : Lean.ParserDescr

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

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

def «termExists_,_» : Lean.ParserDescr

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

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

def «term_×__1» : Lean.ParserDescr

def «term_×'_» : Lean.ParserDescr

def calcFirstStep : Lean.ParserDescr

def calcStep : Lean.ParserDescr

def calcSteps : Lean.ParserDescr

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 \n _ = := . 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.

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 \n _ = := . 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.

def unexpandUnit : Lean.PrettyPrinter.Unexpander

def unexpandListNil : Lean.PrettyPrinter.Unexpander

def unexpandListCons : Lean.PrettyPrinter.Unexpander

def unexpandListToArray : Lean.PrettyPrinter.Unexpander

def unexpandProdMk : Lean.PrettyPrinter.Unexpander

def unexpandIte : Lean.PrettyPrinter.Unexpander

def unexpandSorryAx : Lean.PrettyPrinter.Unexpander

def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander

def unexpandEqRec : Lean.PrettyPrinter.Unexpander

def unexpandExists : Lean.PrettyPrinter.Unexpander

def unexpandSigma : Lean.PrettyPrinter.Unexpander

def unexpandPSigma : Lean.PrettyPrinter.Unexpander

def unexpandSubtype : Lean.PrettyPrinter.Unexpander

def unexpandTSyntax : Lean.PrettyPrinter.Unexpander

def unexpandTSyntaxArray : Lean.PrettyPrinter.Unexpander

def unexpandTSepArray : Lean.PrettyPrinter.Unexpander

def unexpandGetElem : Lean.PrettyPrinter.Unexpander

def unexpandGetElem! : Lean.PrettyPrinter.Unexpander

def unexpandGetElem? : Lean.PrettyPrinter.Unexpander

def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander

def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander

def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander

def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander

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.

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

Expands

class abbrev C  := D_1, ..., D_n

into

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

def cdotTk : Lean.ParserDescr

def cdot : Lean.ParserDescr

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

def solve : Lean.ParserDescr

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

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 β

@[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

def Lean.doElemRepeat_ : Lean.ParserDescr

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

def Lean.doElemWhile_Do_ : Lean.ParserDescr

def Lean.doElemRepeat__Until_ : Lean.ParserDescr

def Lean.«term_Matches_|» : Lean.TrailingParserDescr