lean2/tests/lean/coercion2.lean
Leonardo de Moura c97e669f0c Add coercion support in the elaborator and pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 19:09:07 -07:00

33 lines
600 B
Text

Set pp::colors false
Variable T : Type
Variable R : Type
Variable t2r : T -> R
Coercion t2r
Variable g : R -> R -> R
Variable a : T
Show g a a
Variable b : R
Show g a b
Show g b a
Set lean::pp::coercion true
Show g a a
Show g a b
Show g b a
Set lean::pp::coercion false
Variable S : Type
Variable s : S
Variable r : S
Variable h : S -> S -> S
Infixl 10 ++ : g
Infixl 10 ++ : h
Set lean::pp::notation false
Show a ++ b ++ a
Show r ++ s ++ r
Check a ++ b ++ a
Check r ++ s ++ r
Set lean::pp::coercion true
Show a ++ b ++ a
Show r ++ s ++ r
Set lean::pp::notation true
Show a ++ b ++ a
Show r ++ s ++ r