max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/metavar_context): metavar_decl as Lean object

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-09 20:35:05 -07:00
parent 5dd3b67a75
commit 99d4b33559
2 changed files with 17 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/metavar_context.cpp
View file

@ -14,6 +14,13 @@ namespace lean {
static name * g_meta_prefix;
static expr * g_dummy_type;
metavar_decl::metavar_decl(name const & user_name, local_context const & lctx, expr const & type):
object_ref(mk_cnstr(0, user_name, lctx, type)) {
}
metavar_decl::metavar_decl():
metavar_decl(name(), local_context(), expr()) {}
static expr mk_meta_ref(name const & n) {
return mk_metavar(n, *g_dummy_type);
}

21
src/library/metavar_context.h
View file

@ -8,18 +8,17 @@ Author: Leonardo de Moura
#include "library/local_context.h"
namespace lean {
class metavar_decl {
name m_user_name;
local_context m_context;
expr m_type;
friend class metavar_context;
metavar_decl(name const & user_name, local_context const & ctx, expr const & type):
m_user_name(user_name), m_context(ctx), m_type(type) {}
class metavar_decl : public object_ref {
public:
metavar_decl() {}
expr const & get_type() const { return m_type; }
local_context const & get_context() const { return m_context; }
name const & get_user_name() const { return m_user_name; }
metavar_decl();
metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
metavar_decl(metavar_decl const & other):object_ref(other) {}
metavar_decl(metavar_decl && other):object_ref(other) {}
metavar_decl & operator=(metavar_decl const & other) { object_ref::operator=(other); return *this; }
metavar_decl & operator=(metavar_decl && other) { object_ref::operator=(other); return *this; }
name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 0)); }
local_context const & get_context() const { return static_cast<local_context const &>(cnstr_get_ref(raw(), 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
};
bool is_metavar_decl_ref(level const & l);