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

fix(kernel/expr): relax macro_definition interface

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-28 14:02:48 -07:00
parent 1b9e2efb0c
commit e62254fbb3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/expr.h
View file

@ -261,9 +261,9 @@ public:
macro_definition():m_rc(0) {} macro_definition():m_rc(0) {}
virtual ~macro_definition() {} virtual ~macro_definition() {}
virtual name get_name() const = 0; virtual name get_name() const = 0;
virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context const & ctx) const = 0; virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context & ctx) const = 0;
virtual optional<expr> expand1(unsigned num, expr const * args, extension_context const & ctx) const = 0; virtual optional<expr> expand1(unsigned num, expr const * args, extension_context & ctx) const = 0;
virtual optional<expr> expand(unsigned num, expr const * args, extension_context const & ctx) const = 0; virtual optional<expr> expand(unsigned num, expr const * args, extension_context & ctx) const = 0;
virtual unsigned trust_level() const { return 0; } virtual unsigned trust_level() const { return 0; }
virtual int push_lua(lua_State * L) const; virtual int push_lua(lua_State * L) const;
virtual bool operator==(macro_definition const & other) const; virtual bool operator==(macro_definition const & other) const;