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

feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this'

Browse source 
This is useful if 'show' is recursive
This commit is contained in:
Leonardo de Moura 2015-08-07 18:25:54 +01:00
parent f9b069b6a5
commit f21647899f
3 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/builtin_exprs.cpp
View file

@ -499,16 +499,15 @@ static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & p
return p.save_pos(Fun(l, body), pos); return p.save_pos(Fun(l, body), pos);
} }
static name * H_show = nullptr;
static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) { static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
expr prop = p.parse_expr(); expr prop = p.parse_expr();
if (p.curr_is_token(get_bar_tk())) { if (p.curr_is_token(get_bar_tk())) {
expr fn = p.save_pos(mk_local(*H_show, prop), pos); expr fn = p.save_pos(mk_local(get_this_tk(), prop), pos);
return parse_local_equations(p, fn); return parse_local_equations(p, fn);
} else { } else {
p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected"); p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected");
expr proof = parse_proof(p, prop); expr proof = parse_proof(p, prop);
expr b = p.save_pos(mk_lambda(*H_show, prop, Var(0)), pos); expr b = p.save_pos(mk_lambda(get_this_tk(), prop, Var(0)), pos);
expr r = p.mk_app(b, proof, pos); expr r = p.mk_app(b, proof, pos);
return p.save_pos(mk_show_annotation(r), pos); return p.save_pos(mk_show_annotation(r), pos);
} }
@ -717,7 +716,6 @@ parse_table init_led_table() {
return r; return r;
} }
} }
bool is_show_aux_name(name const & n) { return n == *notation::H_show; }
static parse_table * g_nud_table = nullptr; static parse_table * g_nud_table = nullptr;
static parse_table * g_led_table = nullptr; static parse_table * g_led_table = nullptr;
@ -731,7 +729,6 @@ parse_table get_builtin_led_table() {
} }
void initialize_builtin_exprs() { void initialize_builtin_exprs() {
notation::H_show = new name("H_show");
notation::H_obtain_from = new name("H_obtain_from"); notation::H_obtain_from = new name("H_obtain_from");
notation::g_not = new expr(mk_constant(get_not_name())); notation::g_not = new expr(mk_constant(get_not_name()));
g_nud_table = new parse_table(); g_nud_table = new parse_table();
@ -743,7 +740,6 @@ void initialize_builtin_exprs() {
void finalize_builtin_exprs() { void finalize_builtin_exprs() {
delete g_led_table; delete g_led_table;
delete g_nud_table; delete g_nud_table;
delete notation::H_show;
delete notation::H_obtain_from; delete notation::H_obtain_from;
delete notation::g_not; delete notation::g_not;
} }

1
src/frontends/lean/builtin_exprs.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
parse_table get_builtin_nud_table(); parse_table get_builtin_nud_table();
parse_table get_builtin_led_table(); parse_table get_builtin_led_table();
bool is_show_aux_name(name const & n);
void initialize_builtin_exprs(); void initialize_builtin_exprs();
void finalize_builtin_exprs(); void finalize_builtin_exprs();
} }

9
tests/lean/run/show2.lean Normal file
View file

@ -0,0 +1,9 @@
import data.nat
open nat
example : ∀ a b, a + b = b + a :=
show ∀ a b : nat, a + b = b + a
| 0 0 := rfl
| 0 (succ b) := by rewrite zero_add
| (succ a) 0 := by rewrite zero_add
| (succ a) (succ b) := by rewrite [succ_add, this]