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

feat(frontends/lean/pp): change how lift local entries are pretty printed

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-06 17:25:33 -08:00
parent a51139e63b
commit ea06bb2885
4 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1096,7 +1096,7 @@ class pp_fn {
for (local_entry const & e : metavar_lctx(a)) {
format e_fmt;
if (e.is_lift()) {
e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())};
e_fmt = format{g_lift_fmt, colon(), format(e.s()), space(), format(e.n())};
} else {
lean_assert(e.is_inst());
auto p_e = pp_child_with_paren(e.v(), depth);

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

@ -23,7 +23,7 @@ x : ?M::0, A : Type ⊢ ?M::0 ≺ A
x
Assumed: my_eq
Failed to solve
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0 3] ≺ C
elab1.lean:13:51: Type of argument 2 must be convertible to the expected type in the application of
my_eq
with arguments:

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

@ -10,7 +10,7 @@ Failed to solve
with arguments:
?M::3
λ m : ℕ, trans (Nat::add_zerol m) (symm (Nat::add_zeror m))
λ (n : ℕ) (iH : (?M::3[lift:0:1]) n) (m : ℕ),
λ (n : ℕ) (iH : (?M::3[lift:0 1]) n) (m : ℕ),
@trans ℕ
(n + 1 + m)
(m + n + 1)
@ -24,7 +24,7 @@ Failed to solve
?M::15
?M::16
(λ x : ?M::14,
@eq ((?M::48[lift:0:1]) x) ((?M::49[lift:0:1]) x) ((?M::50[lift:0:1]) x))
@eq ((?M::48[lift:0 1]) x) ((?M::49[lift:0 1]) x) ((?M::50[lift:0 1]) x))
(refl (n + m + 1))
iH))
(symm (Nat::add_succr m n))

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

@ -3,7 +3,7 @@
Assumed: f
λ (A B : Type) (a : B), f B a
Failed to solve
A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B
A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0 2] ≺ B
tst7.lean:4:42: Type of argument 2 must be convertible to the expected type in the application of
f
with arguments: