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

fix(kernel/level): initialization error

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-28 11:03:23 -07:00
parent 2ddadfc920
commit e3b79730ba
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/level.cpp
View file

@ -205,13 +205,17 @@ level mk_meta_univ(name const & n) {
return level(new level_param_core(false, n));
}
static level g_zero(new level_cell(level_kind::Zero, 7u));
static level g_one(mk_succ(g_zero));
level const & mk_level_zero() {
static level g_zero(new level_cell(level_kind::Zero, 7u));
return g_zero;
}
level const & mk_level_zero() { return g_zero; }
level const & mk_level_one() { return g_one; }
level const & mk_level_one() {
static level g_one(mk_succ(mk_level_zero()));
return g_one;
}
level::level():level(g_zero) {}
level::level():level(mk_level_zero()) {}
level::level(level_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); }
level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
level::level(level && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }