lean2/tests/lean/norm_tac.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
  Set: lean::pp::implicit
  Set: lean::pp::coercion
  Set: lean::pp::notation
  Assumed: vector
  Assumed: read
  Assumed: V1
  Defined: D
Definition D : ℤ := @read ℤ 10 V1 1 Trivial
  Assumed: b
  Defined: a
  Proved: T
-												feat(library/tactic): add normalize_tac, eval_tac and trivial_tac

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-22 22:10:42 +00:00
+								  Set: pp::colors
 								  Set: pp::unicode
-												fix(tests/lean/norm_tac): display implicit parameters to make sure output can be parsed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-23 01:11:36 +00:00
+								  Set: lean::pp::implicit
-												feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-23 01:57:51 +00:00
+								  Set: lean::pp::coercion
 								  Set: lean::pp::notation
-												feat(library/tactic): add normalize_tac, eval_tac and trivial_tac

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-22 22:10:42 +00:00
+								  Assumed: vector
 								  Assumed: read
 								  Assumed: V1
 								  Defined: D
-												feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-23 01:57:51 +00:00
+								Definition D : ℤ := @read ℤ 10 V1 1 Trivial
-												feat(library/tactic): add normalize_tac, eval_tac and trivial_tac

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2013-12-22 22:10:42 +00:00
+								  Assumed: b
 								  Defined: a
 								  Proved: T