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

chore(kernel): remove unnecessary files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-18 14:25:03 -07:00
parent d0dc16355b
commit ee58a83e25
2 changed files with 0 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/kernel/kernel.cpp
View file

@ -1,46 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/kernel.h"
#include "kernel/environment.h"
#include "kernel/abstract.h"
#include "kernel/io_state.h"
#include "kernel/decl_macros.h"
#include "kernel/kernel_decls.cpp"
namespace lean {
// =======================================
// Bultin universe variables m and u
static level u_lvl(name("U"));
expr const TypeU = Type(u_lvl);
expr const TypeU1 = Type(u_lvl+1);
// =======================================
// =======================================
// Boolean Type
expr const Bool = mk_Bool();
expr const True = mk_true();
expr const False = mk_false();
expr mk_bool_type() { return mk_Bool(); }
bool is_bool(expr const & t) { return is_Bool(t); }
// =======================================
expr mk_bool_value(bool v) {
return v ? True : False;
}
bool is_bool_value(expr const & e) {
return is_true(e) || is_false(e);
}
bool to_bool(expr const & e) {
lean_assert(is_bool_value(e));
return e == True;
}
// =======================================
void import_kernel(environment const & env, io_state const & ios) {
env->import("kernel", ios);
}
}

41
src/kernel/kernel.h
View file

@ -1,41 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/io_state.h"
#include "kernel/kernel_decls.h"
namespace lean {
// See src/builtin/kernel.lean for signatures.
extern expr const TypeU;
extern expr const TypeU1; // Type (U+1)
/** \brief Return the Lean Boolean type. */
expr mk_bool_type();
extern expr const Bool;
bool is_bool(expr const & e);
/** \brief Create a Lean Boolean value (true/false) */
expr mk_bool_value(bool v);
extern expr const True;
extern expr const False;
/** \brief Return true iff \c e is a Lean Boolean value. */
bool is_bool_value(expr const & e);
/**
\brief Convert a Lean Boolean value into a C++ Boolean value.
\pre is_bool_value(e)
*/
bool to_bool(expr const & e);
inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); }
inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
inline expr Not(expr const & e) { return mk_not(e); }
inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
// inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_eq(A, l, r); }
void import_kernel(environment const & env, io_state const & ios);
}