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

feat(library/abstract_parser): add parse_name virtual method

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-24 13:54:05 -08:00
parent 8ac423768c
commit 214471a2c9
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.h
View file

@ -326,6 +326,8 @@ public:
unsigned get_small_nat();
virtual unsigned parse_small_nat() override final;
virtual std::string parse_string_lit() override final;
virtual name parse_name() override final { return check_id_next("identifier expected"); }
double parse_double();
bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); }

1
src/library/abstract_parser.h
View file

@ -35,6 +35,7 @@ public:
virtual unsigned parse_small_nat() = 0;
virtual std::string parse_string_lit() = 0;
virtual name parse_name() = 0;
/** Always parses an expression. Returns a synthetic sorry even if no input is consumed. */
virtual expr parse_expr(unsigned rbp = 0) = 0;
};