Helper functions for backend code generators #
Return true iff b is of the form let x := g ys; ret x
Instances For
Instances For
@[inline]
Instances For
Instances For
Instances For
def
Lean.IR.collectUsedDecls
(env : Lean.Environment)
(decl : Lean.IR.Decl)
(used : optParam Lean.NameSet ∅)
:
Instances For
@[inline]
Instances For
Instances For
@[inline]
Instances For
collectFnBody assumes the variables in
Instances For
Return a pair (v, j), where v is a mapping from variable/parameter to type,
and j is a mapping from join point to parameters.
This function assumes d has normalized indexes (see normids.lean).