max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: LCNF imports

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-23 06:41:03 -07:00
parent 4323205185
commit aa17641f18
1 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/Lean/Compiler/LCNF.lean
View file

@ -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