diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index ca7983c6e7..0390bbcfad 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -101,9 +101,16 @@ The `PassManager` used to store all `Pass`es that will be run within pipeline. -/ structure PassManager where + /-- Passes that happen during the LCNF base phase -/ basePasses : Array Pass + /-- Passes that happen during the LCNF mono phase before lambda lifting -/ monoPasses : Array Pass + /-- + Passes that happen during the LCNF mono phase after lambda lifting. Note that lifted lambdas will + have been lifted out of the SCC they originated from if possible. + -/ monoPassesNoLambda : Array Pass + /-- Passes that happen during the LCNF impure phase. -/ impurePasses : Array Pass deriving Inhabited