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

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