From b41d7ec98b59261a60a8434df939637ca3e04771 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 May 2019 15:20:56 -0700 Subject: [PATCH] chore(library/compiler/ir): style --- src/library/compiler/ir.cpp | 3 ++- src/library/compiler/ir.h | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 601fd3a210..560285a27d 100644 --- a/src/library/compiler/ir.cpp +++ b/src/library/compiler/ir.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/array_ref.h" #include "util/nat.h" #include "kernel/instantiate.h" @@ -393,7 +394,7 @@ class to_ir_fn { lean_assert(!is_fvar(val)); if (is_lit(val)) { return visit_lit(decl, b); - } if (is_lambda(val)) { + } else if (is_lambda(val)) { return visit_jp(decl, b); } else { expr const & fn = get_app_fn(val); diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h index 16e393491a..a7d46e4750 100644 --- a/src/library/compiler/ir.h +++ b/src/library/compiler/ir.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "kernel/environment.h" #include "library/compiler/util.h" namespace lean {