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

Fix test error on Cygwin

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-09 18:35:11 -07:00
parent d912c9cd09
commit 4c67721d32
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/lean_parser.cpp
View file

@ -1204,7 +1204,7 @@ class parser::imp {
formatter fmt = m_frontend.get_state().get_formatter();
options opts = m_frontend.get_state().get_options();
unsigned indent = get_pp_indent(opts);
format r = group(format{fmt(v), space(), colon(), nest(indent, compose(line(), fmt(t)))});
format r = group(format{fmt(v, opts), space(), colon(), nest(indent, compose(line(), fmt(t, opts)))});
regular(m_frontend) << mk_pair(r, opts) << endl;
}

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

@ -22,8 +22,8 @@ g b (t2r a)
Set: lean::pp::notation
g (g a b) a
h (h r s) r
a ++ b ++ a : R
r ++ s ++ r : S
g (g a b) a : R
h (h r s) r : S
Set: lean::pp::coercion
g (g (t2r a) b) (t2r a)
h (h r s) r

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

@ -9,7 +9,7 @@ f::explicit N n1 n2
f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
Assumed: EqNice
EqNice::explicit N n1 n2
f n1 n2 : N
f::explicit N n1 n2 : N
Congr::explicit :
Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
f::explicit N n1 n2