Documentation

Init.NotationExtra

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

Lean.ParserDescr

Equations

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

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? (Array.size idents) body

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

Equations

Lean.expandBrackedBindersAux combinator binders body = Lean.expandBrackedBindersAux.loop combinator binders (Array.size binders) body

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 : Lean.Name) (explicitBinders : Lean.Syntax) (body : Lean.Syntax) :

Lean.MacroM 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) :

Lean.MacroM Lean.Syntax

Equations

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

def Lean.unifConstraint:

Lean.ParserDescr

Equations

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

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

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_×'_»:

Lean.ParserDescr

Equations

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

Lean.ParserDescr

Equations

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

def calc:

Lean.ParserDescr

Equations

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

def tacticCalc_:

Lean.ParserDescr

Equations

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

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

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

Lean.ParserDescr

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying new 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 «command_ClassAbbrev__:_:=__,»:

Lean.ParserDescr

Equations

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

def «tactic·.__;_»:

Lean.ParserDescr

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

Equations

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

def solve:

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.

inductive Lean.Loop:

Type

mk: Lean.Loop

@[inline]

def Lean.Loop.forIn {β : Type u} {m : Type u → Type v} [inst : Monad m] :

Lean.Loop → β → (Unit → β → m (ForInStep β)) → m β

Equations

Lean.Loop.forIn x init f = Lean.Loop.forIn.loop f init

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

ForIn m Lean.Loop Unit

Equations

Lean.instForInLoopUnit = { forIn := fun {β} [Monad m] => Lean.Loop.forIn }

def Lean.doElemRepeat_:

Lean.ParserDescr

Equations

Lean.doElemRepeat_ = Lean.ParserDescr.node `Lean.doElemRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "repeat ") (Lean.ParserDescr.const `doSeq))

def Lean.doElemWhile_Do_:

Lean.ParserDescr

Equations

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

def Lean.doElemRepeat_Until_:

Lean.ParserDescr

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.