Documentation

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

def Lean.binderIdent :

def Lean.unbracketedExplicitBinders :

def Lean.bracketedExplicitBinders :

def Lean.explicitBinders :

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

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

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

def Lean.expandBrackedBindersAux.loop (combinator : Lean.Syntax) (binders : Array Lean.Syntax) (i : Nat) (acc : Lean.Syntax) :

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

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

def Lean.unifConstraint :

def Lean.unifConstraintElem :

def Lean.«command_Unif_hint___Where_|-⊢_» :

def «term∃_,_» :

def «termExists_,_» :

def «termΣ_,_» :

def «termΣ'_,_» :

def «term_×__1» :

def «term_×'_» :

def calcStep :

def calc :

def tacticCalc_ :

def unexpandUnit :

def unexpandListNil :

def unexpandListCons :

def unexpandListToArray :

def unexpandProdMk :

def unexpandIte :

def unexpandSorryAx :

def unexpandEqNDRec :

def unexpandEqRec :

def unexpandExists :

def unexpandSigma :

def unexpandPSigma :

def unexpandSubtype :

def tacticFunext__ :

def «command_ClassAbbrev__:_:=__,» :

def «tactic·.__;_» :

def solve :