From 1c30c68d2df5d16a341037edfadc249baeb53ac5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Aug 2013 09:02:45 -0700 Subject: [PATCH] Refine toplevel API Signed-off-by: Leonardo de Moura --- src/exprlib/toplevel.cpp | 9 ++++++--- src/exprlib/toplevel.h | 6 +++--- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/exprlib/toplevel.cpp b/src/exprlib/toplevel.cpp index 653b259e3..c922a648a 100644 --- a/src/exprlib/toplevel.cpp +++ b/src/exprlib/toplevel.cpp @@ -10,11 +10,14 @@ Author: Leonardo de Moura #include "arith.h" namespace lean { +void init_toplevel(environment & env) { + add_basic_theory(env); + add_basic_thms(env); + add_int_theory(env); +} environment mk_toplevel() { environment r; - add_basic_theory(r); - add_basic_thms(r); - add_int_theory(r); + init_toplevel(r); return r; } } diff --git a/src/exprlib/toplevel.h b/src/exprlib/toplevel.h index 408db2472..11a60f306 100644 --- a/src/exprlib/toplevel.h +++ b/src/exprlib/toplevel.h @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "environment.h" namespace lean { -/** - \brief Create top-level environment with builtin objects. -*/ +/** \brief Initialize environment with builtin objects and basic theorems. */ +void init_toplevel(environment & env); +/** \brief Create top-level environment with builtin objects and basic theorems. */ environment mk_toplevel(); }