Documentation

Lean.Meta.Closure

source
structure Lean.Meta.Closure.ToProcessElement:
Type
source
instance Lean.Meta.Closure.instInhabitedToProcessElement:
Inhabited Lean.Meta.Closure.ToProcessElement
Equations
source
structure Lean.Meta.Closure.Context:
Type
source
structure Lean.Meta.Closure.State:
Type
source
@[inline]
abbrev Lean.Meta.Closure.ClosureM (α : Type) :
Type
Equations
source
@[inline]
def Lean.Meta.Closure.visitLevel (f : Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level) (u : Lean.Level) :
Lean.Meta.Closure.ClosureM Lean.Level
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Meta.Closure.visitExpr (f : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr) (e : Lean.Expr) :
Lean.Meta.Closure.ClosureM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.mkNewLevelParam (u : Lean.Level) :
Lean.Meta.Closure.ClosureM Lean.Level
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.Closure.collectLevelAux:
Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level
source
def Lean.Meta.Closure.collectLevel (u : Lean.Level) :
Lean.Meta.Closure.ClosureM Lean.Level
Equations
source
def Lean.Meta.Closure.preprocess (e : Lean.Expr) :
Lean.Meta.Closure.ClosureM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.mkNextUserName:
Lean.Meta.Closure.ClosureM Lean.Name

Remark: This method does not guarantee unique user names. The correctness of the procedure does not rely on unique user names. Recall that the pretty printer takes care of unintended collisions.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.pushToProcess (elem : Lean.Meta.Closure.ToProcessElement) :
Lean.Meta.Closure.ClosureM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.Closure.collectExprAux (e : Lean.Expr) :
Lean.Meta.Closure.ClosureM Lean.Expr
source
def Lean.Meta.Closure.collectExpr (e : Lean.Expr) :
Lean.Meta.Closure.ClosureM Lean.Expr
Equations
source
partial def Lean.Meta.Closure.pickNextToProcessAux (lctx : Lean.LocalContext) (i : Nat) (toProcess : Array Lean.Meta.Closure.ToProcessElement) (elem : Lean.Meta.Closure.ToProcessElement) :
Lean.Meta.Closure.ToProcessElement × Array Lean.Meta.Closure.ToProcessElement
source
def Lean.Meta.Closure.pickNextToProcess?:
Lean.Meta.Closure.ClosureM (Option Lean.Meta.Closure.ToProcessElement)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.pushFVarArg (e : Lean.Expr) :
Lean.Meta.Closure.ClosureM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.pushLocalDecl (newFVarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) :
Lean.Meta.Closure.ClosureM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.Closure.process:
Lean.Meta.Closure.ClosureM Unit
source
@[inline]
def Lean.Meta.Closure.mkBinding (isLambda : Bool) (decls : Array Lean.LocalDecl) (b : Lean.Expr) :
Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.mkLambda (decls : Array Lean.LocalDecl) (b : Lean.Expr) :
Lean.Expr
Equations
source
def Lean.Meta.Closure.mkForall (decls : Array Lean.LocalDecl) (b : Lean.Expr) :
Lean.Expr
Equations
source
structure Lean.Meta.Closure.MkValueTypeClosureResult:
Type
source
def Lean.Meta.Closure.mkValueTypeClosureAux (type : Lean.Expr) (value : Lean.Expr) :
Lean.Meta.Closure.ClosureM (Lean.Expr × Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Closure.mkValueTypeClosure (type : Lean.Expr) (value : Lean.Expr) (zeta : Bool) :
Lean.MetaM Lean.Meta.Closure.MkValueTypeClosureResult
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.mkAuxDefinition (name : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (zeta : optParam Bool false) (compile : optParam Bool true) :
Lean.MetaM Lean.Expr

Create an auxiliary definition with the given name, type and value. The parameters type and value may contain free and meta variables. A "closure" is computed, and a term of the form name.{u_1 ... u_n} t_1 ... t_m is returned where u_is are universe parameters and metavariables type and value depend on, and t_js are free and meta variables type and value depend on.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.mkAuxDefinitionFor (name : Lean.Name) (value : Lean.Expr) (zeta : optParam Bool false) :
Lean.MetaM Lean.Expr

Similar to mkAuxDefinition, but infers the type of value.

Equations