# Documentation

Lean.Compiler.LCNF.Simp.Used

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.

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.

Mark all free variables occurring in arg as used.

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

Mark all free variables occurring in e as used.

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

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

Mark all free variables occurring in code as used.

Mark all free variables occurring in funDecl as used.

Return true if fvarId is in the used set.

Equations

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


Equations
• Lean.Compiler.LCNF.Simp.attachCodeDecls decls code = Lean.Compiler.LCNF.Simp.attachCodeDecls.go decls (Array.size decls) code
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.