lean2/tests/lean/coercion2.lean.expected.out
Leonardo de Moura 4c67721d32 Fix test error on Cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 18:35:11 -07:00

32 lines
502 B
Text

Set: pp::colors
Set: pp::unicode
Assumed: T
Assumed: R
Assumed: t2r
Coercion t2r
Assumed: g
Assumed: a
g a a
Assumed: b
g a b
g b a
Set: lean::pp::coercion
g (t2r a) (t2r a)
g (t2r a) b
g b (t2r a)
Set: lean::pp::coercion
Assumed: S
Assumed: s
Assumed: r
Assumed: h
Set: lean::pp::notation
g (g a b) a
h (h r s) r
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
Set: lean::pp::notation
(t2r a) ++ b ++ (t2r a)
r ++ s ++ r