michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean): move type_checker_ptr typedef to library

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 14:40:15 -08:00
parent 02de288a51
commit caf0a4bf15
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/util.h
View file

@ -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> type_checker_ptr;
/** \brief Parse optional '[persistent]' modifier.
return true if it is was found, and paremeter \c persistent to true.
*/

3
src/library/util.h
View file

@ -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> type_checker_ptr;
bool has_unit_decls(environment const & env);
bool has_eq_decls(environment const & env);
bool has_heq_decls(environment const & env);