def Lean.unbracketedExplicitBinders : ParserDescr

Equations

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

def Lean.bracketedExplicitBinders : ParserDescr

Equations

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

def Lean.explicitBinders : ParserDescr

Equations

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

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

Equations

• Lean.expandExplicitBindersAux combinator idents type? body = Lean.expandExplicitBindersAux.loop combinator idents type? idents.size ⋯ body

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

Equations

• Lean.expandBrackedBindersAux combinator binders body = Lean.expandBrackedBindersAux.loop combinator binders binders.size ⋯ body

def Lean.expandBrackedBindersAux.loop (combinator : Syntax) (binders : Array Syntax) (i : Nat) (h : i ≤ binders.size) (acc : Syntax) : MacroM 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 : Name) (explicitBinders body : Syntax) : MacroM Syntax

Equations

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

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

Equations

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

def Lean.unifConstraint : ParserDescr

Equations

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

def Lean.unifConstraintElem : ParserDescr

Equations

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

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

Equations

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

def Lean.calcFirstStep : ParserDescr

Equations

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

def Lean.calcStep : ParserDescr

Equations

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

def Lean.calcSteps : ParserDescr

Equations

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

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.

Equations

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

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.

Equations

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

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.

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

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 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 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 : 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 Lean.cdotTk : ParserDescr

Equations

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

def Lean.cdot : ParserDescr

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

Equations

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

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

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 Lean.singletonUnexpander : PrettyPrinter.Unexpander

Unexpander for the { x } notation.

Equations

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

def Lean.insertUnexpander : PrettyPrinter.Unexpander

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

Equations

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