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

feat(library/util): disable local constant purification when pretty printing goals

Browse source 
This feature generates confusion.
This commit is contained in:
Leonardo de Moura 2015-07-23 18:43:56 -07:00
parent f1a19a10c4
commit 3e6b80d38c
3 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/util.cpp
View file

@ -822,9 +822,11 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
});
}
format format_goal(formatter const & fmt, buffer<expr> const & hyps, expr const & conclusion, substitution const & s) {
format format_goal(formatter const & _fmt, buffer<expr> const & hyps, expr const & conclusion, substitution const & s) {
substitution tmp_subst(s);
options const & opts = fmt.get_options();
options opts = _fmt.get_options();
opts = opts.update_if_undef(get_pp_purify_locals_name(), false);
formatter fmt = _fmt.update_options(opts);
unsigned indent = get_pp_indent(opts);
bool unicode = get_pp_unicode(opts);
bool compact = get_pp_compact_goals(opts);

2
tests/lean/assert_fail.lean.expected.out
View file

@ -4,7 +4,7 @@ H : b ∧ a
⊢ a
a b : Prop,
H_1 : b ∧ a,
H : b ∧ a,
H : a
⊢ a ∧ b
assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables

4
tests/lean/assert_tac2.lean.expected.out
View file

@ -2,7 +2,7 @@ assert_tac2.lean:11:2: proof state
a b c : ℕ,
h1 : a = 2,
h2 : b = 3,
H_2 : a + b = 2 + b,
H_1 : a + b = 2 + 3,
H : a + b = 2 + b,
H : a + b = 2 + 3,
H : a + b = 5
⊢ 5 + c = c + 5