From 79683c4bf6dc51ddbbcbfde9a1419b7edd4db439 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Oct 2022 18:11:19 -0700 Subject: [PATCH] chore: missing imports --- src/Lean/Compiler/LCNF.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean index e69c59f75f..dd005b63b0 100644 --- a/src/Lean/Compiler/LCNF.lean +++ b/src/Lean/Compiler/LCNF.lean @@ -36,4 +36,6 @@ import Lean.Compiler.LCNF.Util import Lean.Compiler.LCNF.ConfigOptions import Lean.Compiler.LCNF.ForEachExpr import Lean.Compiler.LCNF.MonoTypes -import Lean.Compiler.LCNF.ToMono \ No newline at end of file +import Lean.Compiler.LCNF.ToMono +import Lean.Compiler.LCNF.MonadScope +import Lean.Compiler.LCNF.Closure \ No newline at end of file