Insert explicit RC instructions. So, it assumes the input code does not contain inc nor dec instructions. This transformation is applied before lower level optimizations that introduce the instructions release and set

structure Lean.IR.ExplicitRC.VarInfo : Type

• ref : Bool
• persistent : Bool
• consume : Bool

instance Lean.IR.ExplicitRC.instInhabitedVarInfo : Inhabited Lean.IR.ExplicitRC.VarInfo

@[inline, reducible]

abbrev Lean.IR.ExplicitRC.VarMap : Type

structure Lean.IR.ExplicitRC.Context : Type

• env : Lean.Environment
• decls : Array Lean.IR.Decl
• varMap : Lean.IR.ExplicitRC.VarMap
• jpLiveVarMap : Lean.IR.JPLiveVarMap
• localCtx : Lean.IR.LocalContext

def Lean.IR.ExplicitRC.getDecl (ctx : Lean.IR.ExplicitRC.Context) (fid : Lean.IR.FunId) : Lean.IR.Decl

def Lean.IR.ExplicitRC.getVarInfo (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) : Lean.IR.ExplicitRC.VarInfo

def Lean.IR.ExplicitRC.getJPParams (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) : Array Lean.IR.Param

def Lean.IR.ExplicitRC.getJPLiveVars (ctx : Lean.IR.ExplicitRC.Context) (j : Lean.IR.JoinPointId) : Lean.IR.LiveVarSet

def Lean.IR.ExplicitRC.mustConsume (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) : Bool

@[inline]

def Lean.IR.ExplicitRC.addInc (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) (n : optParam Nat 1) : Lean.IR.FnBody

@[inline]

def Lean.IR.ExplicitRC.addDec (ctx : Lean.IR.ExplicitRC.Context) (x : Lean.IR.VarId) (b : Lean.IR.FnBody) : Lean.IR.FnBody

def Lean.IR.ExplicitRC.updateVarInfoWithParams (ctx : Lean.IR.ExplicitRC.Context) (ps : Array Lean.IR.Param) : Lean.IR.ExplicitRC.Context

partial def Lean.IR.ExplicitRC.visitFnBody : Lean.IR.FnBody → Lean.IR.ExplicitRC.Context → Lean.IR.FnBody × Lean.IR.LiveVarSet

def Lean.IR.ExplicitRC.visitDecl (env : Lean.Environment) (decls : Array Lean.IR.Decl) (d : Lean.IR.Decl) : Lean.IR.Decl

def Lean.IR.explicitRC (decls : Array Lean.IR.Decl) : Lean.IR.CompilerM (Array Lean.IR.Decl)