Documentation

Lean.Compiler.Util

def Lean.Compiler.neutralExpr:

Equations

Lean.Compiler.neutralExpr = Lean.mkConst `_neutral

def Lean.Compiler.unreachableExpr:

Equations

Lean.Compiler.unreachableExpr = Lean.mkConst `_unreachable

def Lean.Compiler.objectType:

Equations

Lean.Compiler.objectType = Lean.mkConst `_obj

def Lean.Compiler.voidType:

Equations

Lean.Compiler.voidType = Lean.mkConst `_void

def Lean.Compiler.mkLcProof (pred : Lean.Expr) :

Equations

Lean.Compiler.mkLcProof pred = Lean.mkApp (Lean.mkConst `lcProof) pred

structure Lean.Compiler.atMostOnce.AtMostOnceData:

Type

found : Bool
result : Bool

def Lean.Compiler.atMostOnce.Visitor:

Type

Equations

Lean.Compiler.atMostOnce.Visitor = (Lean.Compiler.atMostOnce.AtMostOnceData → Lean.Compiler.atMostOnce.AtMostOnceData)

@[inline]

def Lean.Compiler.atMostOnce.seq (f : Lean.Compiler.atMostOnce.Visitor) (g : Lean.Compiler.atMostOnce.Visitor) :

Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.seq f g d = match f d with | { found := found, result := false } => { found := found, result := false } | other => g other

instance Lean.Compiler.atMostOnce.instAndThenVisitor:

AndThen Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.instAndThenVisitor = { andThen := fun a b => Lean.Compiler.atMostOnce.seq a (b ()) }

@[inline]

def Lean.Compiler.atMostOnce.skip:

Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.skip = id

@[inline]

def Lean.Compiler.atMostOnce.visitFVar (x : Lean.FVarId) (y : Lean.FVarId) :

Lean.Compiler.atMostOnce.Visitor

Equations

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

def Lean.Compiler.atMostOnce.visit (x : Lean.FVarId) :

Lean.Expr → Lean.Compiler.atMostOnce.Visitor

@[export lean_at_most_once]

def Lean.Compiler.atMostOnce (e : Lean.Expr) (x : Lean.FVarId) :

Return true iff the free variable with id x occurs at most once in e

Equations

Lean.Compiler.atMostOnce e x = match Lean.Compiler.atMostOnce.visit x e { found := false, result := true } with | { found := found, result := result } => result

@[export lean_mk_eager_lambda_lifting_name]

def Lean.Compiler.mkEagerLambdaLiftingName (n : Lean.Name) (idx : Nat) :

Equations

Lean.Compiler.mkEagerLambdaLiftingName n idx = Lean.Name.mkStr n ("_elambda_" ++ toString idx)

@[export lean_is_eager_lambda_lifting_name]

def Lean.Compiler.isEagerLambdaLiftingName:

Lean.Name → Bool

def Lean.Compiler.checkIsDefinition (env : Lean.Environment) (n : Lean.Name) :

Except String Unit

Equations

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

@[export lean_mk_unsafe_rec_name]

def Lean.Compiler.mkUnsafeRecName (declName : Lean.Name) :

We generate auxiliary unsafe definitions for regular recursive definitions. The auxiliary unsafe definition has a clear runtime cost execution model. This function returns the auxiliary unsafe definition name for the given name.

Equations

Lean.Compiler.mkUnsafeRecName declName = Lean.Name.mkStr declName "_unsafe_rec"

@[export lean_is_unsafe_rec_name]

def Lean.Compiler.isUnsafeRecName?:

Lean.Name → Option Lean.Name

Return some _ if the given name was created using mkUnsafeRecName

Equations

Lean.Compiler.isUnsafeRecName? _fun_discr = match _fun_discr with | Lean.Name.str n "_unsafe_rec" a => some n | x => none