diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index fd621873f..4d895c958 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/src/frontends/lean/notation_cmd.h @@ -10,14 +10,6 @@ Author: Leonardo de Moura #include "frontends/lean/cmd_table.h" namespace lean { 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 */ bool curr_is_notation_decl(parser & p); /** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */