From aa17641f18da3617f690815635f5c47db2a80ced Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2022 06:41:03 -0700 Subject: [PATCH] chore: LCNF imports --- src/Lean/Compiler/LCNF.lean | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean index bc0a788a0e..1cba0282bc 100644 --- a/src/Lean/Compiler/LCNF.lean +++ b/src/Lean/Compiler/LCNF.lean @@ -3,21 +3,34 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +import Lean.Compiler.LCNF.AlphaEqv import Lean.Compiler.LCNF.Basic import Lean.Compiler.LCNF.Bind import Lean.Compiler.LCNF.Check import Lean.Compiler.LCNF.CompilerM +import Lean.Compiler.LCNF.CSE +import Lean.Compiler.LCNF.DependsOn import Lean.Compiler.LCNF.ElimDead +import Lean.Compiler.LCNF.FixedArgs import Lean.Compiler.LCNF.InferType +import Lean.Compiler.LCNF.JoinPoints import Lean.Compiler.LCNF.LCtx +import Lean.Compiler.LCNF.Level import Lean.Compiler.LCNF.Main +import Lean.Compiler.LCNF.Passes +import Lean.Compiler.LCNF.PassManager +import Lean.Compiler.LCNF.PhaseExt import Lean.Compiler.LCNF.PrettyPrinter +import Lean.Compiler.LCNF.PullFunDecls +import Lean.Compiler.LCNF.PullLetDecls +import Lean.Compiler.LCNF.ReduceJpArity +import Lean.Compiler.LCNF.Simp +import Lean.Compiler.LCNF.Specialize +import Lean.Compiler.LCNF.SpecInfo +import Lean.Compiler.LCNF.Stage1 +import Lean.Compiler.LCNF.Testing import Lean.Compiler.LCNF.ToDecl import Lean.Compiler.LCNF.ToExpr import Lean.Compiler.LCNF.ToLCNF import Lean.Compiler.LCNF.Types import Lean.Compiler.LCNF.Util -import Lean.Compiler.LCNF.Main -import Lean.Compiler.LCNF.Testing -import Lean.Compiler.LCNF.FixedArgs -import Lean.Compiler.LCNF.SpecInfo