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

refactor(kernel/declaration): return reference to type/value/name

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-25 12:17:04 -07:00
parent d4236e40b4
commit 1d92097781
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/declaration.cpp
View file

@ -54,12 +54,12 @@ bool declaration::is_var_decl() const { return !is_definition(); }
bool declaration::is_axiom() const { return is_var_decl() && m_ptr->m_theorem; }
bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
name declaration::get_name() const { return m_ptr->m_name; }
name const & declaration::get_name() const { return m_ptr->m_name; }
level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; }
expr declaration::get_type() const { return m_ptr->m_type; }
expr const & declaration::get_type() const { return m_ptr->m_type; }
bool declaration::is_opaque() const { return m_ptr->m_opaque; }
expr declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned declaration::get_weight() const { return m_ptr->m_weight; }
module_idx declaration::get_module_idx() const { return m_ptr->m_module_idx; }
bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }

6
src/kernel/declaration.h
View file

@ -59,11 +59,11 @@ public:
bool is_theorem() const;
bool is_var_decl() const;
name get_name() const;
name const & get_name() const;
level_param_names const & get_univ_params() const;
expr get_type() const;
expr const & get_type() const;
expr get_value() const;
expr const & get_value() const;
bool is_opaque() const;
unsigned get_weight() const;
module_idx get_module_idx() const;