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

refactor(frontends/lean): do not expose unnecessary functions

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-11 16:17:40 -07:00
parent f832212fc8
commit 334a4c84d1
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/notation_cmd.h
View file

@ -10,14 +10,6 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h" #include "frontends/lean/cmd_table.h"
namespace lean { namespace lean {
class parser; class parser;
environment precedence_cmd(parser & p);
environment notation_cmd_core(parser & p, bool overload);
environment infixl_cmd_core(parser & p, bool overload);
environment infixr_cmd_core(parser & p, bool overload);
environment postfix_cmd_core(parser & p, bool overload);
environment prefix_cmd_core(parser & p, bool overload);
/** \brief Return true iff the current token is a notation declaration */ /** \brief Return true iff the current token is a notation declaration */
bool curr_is_notation_decl(parser & p); bool curr_is_notation_decl(parser & p);
/** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */ /** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */