lean4-htt/src/Lean/Compiler/LCNF.lean
2022-09-11 20:19:44 -07:00

23 lines
766 B
Text

/-
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.Basic
import Lean.Compiler.LCNF.Bind
import Lean.Compiler.LCNF.Check
import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.ElimDead
import Lean.Compiler.LCNF.InferType
import Lean.Compiler.LCNF.LCtx
import Lean.Compiler.LCNF.Main
import Lean.Compiler.LCNF.PrettyPrinter
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