def Lean.Compiler.LCNF.Simp.markUsedFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark fvarId as an used free variable. This is information is used to eliminate dead local declarations.

Equations

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

def Lean.Compiler.LCNF.Simp.markUsedType (type : Lean.Expr) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in type as used. This is information is used to eliminate dead local declarations.

Equations

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

def Lean.Compiler.LCNF.Simp.markUsedArg (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in arg as used.

Equations

• Lean.Compiler.LCNF.Simp.markUsedArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.Simp.markUsedFVar fvarId
• Lean.Compiler.LCNF.Simp.markUsedArg (Lean.Compiler.LCNF.Arg.type type) = Lean.Compiler.LCNF.Simp.markUsedType type
• Lean.Compiler.LCNF.Simp.markUsedArg Lean.Compiler.LCNF.Arg.erased = pure ()

def Lean.Compiler.LCNF.Simp.markUsedLetValue (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in e as used.

Equations

• Lean.Compiler.LCNF.Simp.markUsedLetValue (Lean.Compiler.LCNF.LetValue.value value) = pure ()
• Lean.Compiler.LCNF.Simp.markUsedLetValue Lean.Compiler.LCNF.LetValue.erased = pure ()
• Lean.Compiler.LCNF.Simp.markUsedLetValue (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId) = Lean.Compiler.LCNF.Simp.markUsedFVar fvarId
• Lean.Compiler.LCNF.Simp.markUsedLetValue (Lean.Compiler.LCNF.LetValue.const declName us args) = Array.forM Lean.Compiler.LCNF.Simp.markUsedArg args
• Lean.Compiler.LCNF.Simp.markUsedLetValue (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = do Lean.Compiler.LCNF.Simp.markUsedFVar fvarId Array.forM Lean.Compiler.LCNF.Simp.markUsedArg args

def Lean.Compiler.LCNF.Simp.markUsedLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring on the right-hand side of the given let declaration as used. This is information is used to eliminate dead local declarations.

Equations

• Lean.Compiler.LCNF.Simp.markUsedLetDecl letDecl = Lean.Compiler.LCNF.Simp.markUsedLetValue letDecl.value

partial def Lean.Compiler.LCNF.Simp.markUsedCode (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in code as used.

partial def Lean.Compiler.LCNF.Simp.markUsedFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.Simp.SimpM Unit

Mark all free variables occurring in funDecl as used.

def Lean.Compiler.LCNF.Simp.isUsed (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.SimpM Bool

Return true if fvarId is in the used set.

Equations

• Lean.Compiler.LCNF.Simp.isUsed fvarId = do let __do_lift ← get pure (Std.HashSet.contains __do_lift.used fvarId)

def Lean.Compiler.LCNF.Simp.attachCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

Attach the given decls to code. For example, assume decls is #[.let _x.1 := 10, .let _x.2 := true], then the result is

let _x.1 := 10
let _x.2 := true
<code>

Equations

• Lean.Compiler.LCNF.Simp.attachCodeDecls decls code = Lean.Compiler.LCNF.Simp.attachCodeDecls.go decls decls.size code

@[irreducible]

def Lean.Compiler.LCNF.Simp.attachCodeDecls.go (decls : Array Lean.Compiler.LCNF.CodeDecl) (i : Nat) (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

Equations

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