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

chore(frontends/lean): remove whitespace

Browse source
This commit is contained in:
Daniel Selsam 2015-10-31 14:51:59 -07:00 committed by Leonardo de Moura
parent fa58d7c71e
commit 6b06a19294
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -699,7 +699,7 @@ static expr parse_partial_explicit_expr(parser & p, unsigned, expr const *, pos_
return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos);
} else {
return p.save_pos(mk_partial_explicit(e), pos);
}
}
}
static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {

2
src/frontends/lean/pp.cpp
View file

@ -153,7 +153,7 @@ void finalize_pp() {
delete g_from_fmt;
delete g_visible_fmt;
delete g_show_fmt;
delete g_partial_explicit_fmt;
delete g_partial_explicit_fmt;
delete g_explicit_fmt;
delete g_tmp_prefix;
}

4
src/library/explicit.cpp
View file

@ -40,13 +40,13 @@ expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args(
void initialize_explicit() {
g_explicit_name = new name("@@");
g_partial_explicit_name = new name("@");
g_partial_explicit_name = new name("@");
g_as_atomic_name = new name("as_atomic");
g_as_is_name = new name("as_is");
g_consume_args_name = new name("!");
register_annotation(*g_explicit_name);
register_annotation(*g_partial_explicit_name);
register_annotation(*g_partial_explicit_name);
register_annotation(*g_as_atomic_name);
register_annotation(*g_as_is_name);
register_annotation(*g_consume_args_name);