lean2/tests/lean/coercion2.lean.expected.out

  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
a ++ b ++ a : R
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
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: pp::colors`
Fix unit tests for Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-03 17:44:51 +00:00			`Set: pp::unicode`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`Assumed: T`
			`Assumed: R`
			`Assumed: t2r`
			`Coercion t2r`
			`Assumed: g`
			`Assumed: a`
			`g a a`
			`Assumed: b`
			`g a b`
			`g b a`
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: lean::pp::coercion`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`g (t2r a) (t2r a)`
			`g (t2r a) b`
			`g b (t2r a)`
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: lean::pp::coercion`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`Assumed: S`
			`Assumed: s`
			`Assumed: r`
			`Assumed: h`
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: lean::pp::notation`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`g (g a b) a`
			`h (h r s) r`
Display the input term in the output of the Check command. It is useful to see the fully elaborated term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-09 05:54:22 +00:00			`a ++ b ++ a : R`
			`r ++ s ++ r : S`
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: lean::pp::coercion`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`g (g (t2r a) b) (t2r a)`
			`h (h r s) r`
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 19:29:21 +00:00			`Set: lean::pp::notation`
Add coercion support in the elaborator and pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-09-02 02:08:49 +00:00			`(t2r a) ++ b ++ (t2r a)`
			`r ++ s ++ r`