Documentation

Lean.Compiler.IR.ResetReuse

@[inline]

abbrev Lean.IR.ResetReuse.M (α : Type) :

Type

Equations

Lean.IR.ResetReuse.M = ReaderT Lean.IR.LocalContext (StateT Lean.IR.Index Id)

partial def Lean.IR.ResetReuse.R :

Lean.IR.FnBody → Lean.IR.ResetReuse.M Lean.IR.FnBody

def Lean.IR.Decl.insertResetReuse (d : Lean.IR.Decl) :

Equations

Lean.IR.Decl.insertResetReuse d = match d with | Lean.IR.Decl.fdecl x x_1 x_2 b x_3 => let nextIndex := Lean.IR.Decl.maxIndex d + 1; let bNew := StateT.run' (Lean.IR.ResetReuse.R b ∅) nextIndex; Lean.IR.Decl.updateBody! d bNew | other => other