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

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

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

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

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

Mark all free variables occurring in arg as used.

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

Mark all free variables occurring in e as used.

def Lean.Compiler.LCNF.Simp.markUsedLetDecl (letDecl : LetDecl) : 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.

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

Mark all free variables occurring in code as used.

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

Mark all free variables occurring in funDecl as used.

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

Return true if fvarId is in the used set.

def Lean.Compiler.LCNF.Simp.attachCodeDecls (decls : Array CodeDecl) (code : Code) : SimpM 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>

@[irreducible]

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