From caf0a4bf15cf1f554841a32d3a0fecead2ced812 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Dec 2014 14:40:15 -0800 Subject: [PATCH] refactor(frontends/lean): move type_checker_ptr typedef to library --- src/frontends/lean/util.h | 4 ++-- src/library/util.h | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index e7a6a8541..1e8273147 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -8,11 +8,11 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/expr_sets.h" #include "kernel/type_checker.h" +#include "library/util.h" #include "frontends/lean/local_decls.h" + namespace lean { class parser; -typedef std::unique_ptr type_checker_ptr; - /** \brief Parse optional '[persistent]' modifier. return true if it is was found, and paremeter \c persistent to true. */ diff --git a/src/library/util.h b/src/library/util.h index a6408aed0..86ebcfc51 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -6,8 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/environment.h" +#include "kernel/type_checker.h" namespace lean { +typedef std::unique_ptr type_checker_ptr; + bool has_unit_decls(environment const & env); bool has_eq_decls(environment const & env); bool has_heq_decls(environment const & env);