Documentation

Init.NotationExtra

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
def Lean.expandExplicitBinders (combinatorDeclName : Lean.Name) (explicitBinders : Lean.Syntax) (body : Lean.Syntax) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.expandBrackedBinders (combinatorDeclName : Lean.Name) (bracketedExplicitBinders : Lean.Syntax) (body : Lean.Syntax) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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

See Theorem Proving in Lean 4 for more information.

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

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 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
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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.

Expands

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

into

class C  extends D_1, ..., D_n
attribute [instance] C.mk
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

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

Equations

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 :
Instances For
    @[inline]
    def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [inst : Monad m] :
    Lean.Loopβ(Unitβm (ForInStep β)) → m β
    Equations
    @[specialize #[]]
    partial def Lean.Loop.forIn.loop {β : Type u} {m : Type u → Type v} [inst : Monad m] (f : Unitβm (ForInStep β)) (b : β) :
    m β
    instance Lean.instForInLoopUnit {m : Type u_1 → Type u_2} :
    Equations
    • Lean.instForInLoopUnit = { forIn := fun {β} [Monad m] => Lean.Loop.forIn }
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.