Skip to content

Commit

Permalink
fix(frontends/lean/definition_cmds): export using_well_founded AST …
Browse files Browse the repository at this point in the history
…node (#784)

Turns out that the ast.json export has been broken this whole time in ignoring definitions which use `using_well_founded`. cc: @gebner , can we get a point release out with this bugfix?
  • Loading branch information
digama0 committed Nov 18, 2022
1 parent cd2d628 commit cb0da9f
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/frontends/lean/definition_cmds.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ expr parse_equation(parser & p, ast_data & parent, expr const & fn) {
optional<expr> parse_using_well_founded(parser & p, ast_data & parent) {
if (p.curr_is_token(get_using_well_founded_tk())) {
auto& data = p.new_ast(get_using_well_founded_tk(), p.pos());
parent.push(data.m_id);
parser::local_scope _(p);
p.clear_expr_locals();
p.next();
Expand Down

0 comments on commit cb0da9f

Please sign in to comment.