diff --git a/bin/version b/bin/version index ee1372d33..717903969 100644 --- a/bin/version +++ b/bin/version @@ -1 +1 @@ -0.2.2 +0.2.3 diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 097ee9263..be895942e 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/src/frontends/lean/parser_config.cpp @@ -122,9 +122,9 @@ token_table const & get_token_table(environment const & env) { serializer & operator<<(serializer & s, action const & a) { s << static_cast(a.kind()); switch (a.kind()) { - case action_kind::Skip: case action_kind::Binder: case action_kind::Binders: + case action_kind::Skip: break; - case action_kind::Expr: + case action_kind::Expr: case action_kind::Binder: case action_kind::Binders: s << a.rbp(); break; case action_kind::Exprs: @@ -159,9 +159,11 @@ action read_action(deserializer & d) { case action_kind::Skip: return notation::mk_skip_action(); case action_kind::Binder: - return notation::mk_binder_action(); + d >> rbp; + return notation::mk_binder_action(rbp); case action_kind::Binders: - return notation::mk_binders_action(); + d >> rbp; + return notation::mk_binders_action(rbp); case action_kind::Expr: d >> rbp; return notation::mk_expr_action(rbp); diff --git a/tests/lean/run/sub_bug.lean b/tests/lean/run/sub_bug.lean new file mode 100644 index 000000000..f21bbba35 --- /dev/null +++ b/tests/lean/run/sub_bug.lean @@ -0,0 +1,3 @@ +import data.subtype data.nat +open nat +check { x : nat | x > 0}