From 234abb1238d1d0370ad98f5e04b854808d183084 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Apr 2014 13:10:05 -0700 Subject: [PATCH] feat(kernel/definition): default constructor for definitions Signed-off-by: Leonardo de Moura --- src/kernel/definition.cpp | 3 +++ src/kernel/definition.h | 9 +++++++++ 2 files changed, 12 insertions(+) diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp index 86980b11c..d64487499 100644 --- a/src/kernel/definition.cpp +++ b/src/kernel/definition.cpp @@ -59,6 +59,9 @@ struct definition::cell { } }; +definition g_dummy = mk_axiom(name(), param_names(), level_cnstrs(), expr()); + +definition::definition():definition(g_dummy) {} definition::definition(cell * ptr):m_ptr(ptr) {} definition::definition(definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } definition::definition(definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } diff --git a/src/kernel/definition.h b/src/kernel/definition.h index 1945581c0..291195d79 100644 --- a/src/kernel/definition.h +++ b/src/kernel/definition.h @@ -20,6 +20,15 @@ class definition { explicit definition(cell * ptr); friend class cell; public: + /** + \brief The default constructor creates a reference to a "dummy" + definition. The actual "dummy" definition is not relevant, and + no procedure should rely on the kind of definition used. + + We have a default constructor because some collections only work + with types that have a default constructor. + */ + definition(); definition(definition const & s); definition(definition && s); ~definition();