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? idents.size ⋯ body

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

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) (h : i ≤ binders.size) (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 h_2 acc = pure acc

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

def Lean.expandBrackedBinders (combinatorDeclName : Lean.Name) (bracketedExplicitBinders 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

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

def «termExists_,_» : Lean.ParserDescr

Equations

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

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

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_×'__1» : Lean.ParserDescr

Equations

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

def Lean.calcFirstStep : Lean.ParserDescr

Equations

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

def Lean.calcStep : Lean.ParserDescr

Equations

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

def Lean.calcSteps : Lean.ParserDescr

Equations

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

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

See Theorem Proving in Lean 4 for more information.

def Lean.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, 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.

Equations

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

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

See Theorem Proving in Lean 4 for more information.

Equations

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

def unexpandUnit : Lean.PrettyPrinter.Unexpander

def unexpandListNil : Lean.PrettyPrinter.Unexpander

Equations

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

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

Equations

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

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

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

def unexpandGetElem? : Lean.PrettyPrinter.Unexpander

def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

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

def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander

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.

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

def Lean.cdotTk : Lean.ParserDescr

def Lean.cdot : Lean.ParserDescr

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

def Lean.solveTactic : 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.

def Lean.«term_Matches_|» : Lean.TrailingParserDescr

Equations

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

def «term{_}» : Lean.ParserDescr

def Lean.singletonUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the { x } notation.

def Lean.insertUnexpander : Lean.PrettyPrinter.Unexpander

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