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

fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-23 17:48:30 -08:00
parent 53d66c91fc
commit 44a2ef8f6f
3 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/version
View file

@ -1 +1 @@
0.2.2
0.2.3

10
src/frontends/lean/parser_config.cpp
View file

@ -122,9 +122,9 @@ token_table const & get_token_table(environment const & env) {
serializer & operator<<(serializer & s, action const & a) {
s << static_cast<char>(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);

3
tests/lean/run/sub_bug.lean Normal file
View file

@ -0,0 +1,3 @@
import data.subtype data.nat
open nat
check { x : nat | x > 0}