def Lean.unbracketedExplicitBinders : ParserDescr

def Lean.bracketedExplicitBinders : ParserDescr

def Lean.explicitBinders : ParserDescr

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

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

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

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

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

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

def Lean.unifConstraint : ParserDescr

def Lean.unifConstraintElem : ParserDescr

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

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

def «termExists_,_» : Lean.ParserDescr

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

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

def «term_×__1» : Lean.ParserDescr

def «term_×'__1» : Lean.ParserDescr

def Lean.calcFirstStep : ParserDescr

def Lean.calcStep : ParserDescr

def Lean.calcSteps : ParserDescr

def Lean.calc : 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 works as a term, as a tactic or as a conv tactic.

See Theorem Proving in Lean 4 for more information.

def Lean.calcTactic : 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 works as a term, as a tactic or as a conv tactic.

See Theorem Proving in Lean 4 for more information.

def Lean.convCalc_ : 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 works as a term, as a tactic or as a conv tactic.

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

Expands

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

into

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

def Lean.cdotTk : ParserDescr

def Lean.cdot : ParserDescr

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

def Lean.solveTactic : ParserDescr

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

def Lean.«term_Matches_|» : TrailingParserDescr

def «term{_}» : Lean.ParserDescr

{ a, b, c } syntax, powered by the Singleton and Insert typeclasses.

Conventions for notations in identifiers:

• The recommended spelling of {x} in identifiers is singleton.

def Lean.singletonUnexpander : PrettyPrinter.Unexpander

Unexpander for the { x } notation.

def Lean.insertUnexpander : PrettyPrinter.Unexpander

Unexpander for the { x, y, ... } notation.