From 477b7b481144580391da1f313ce5967c8a46a205 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Aug 2014 17:55:42 -0700 Subject: [PATCH] fix(tests/lean/run/class_coe): adjust test to reflect library changes Signed-off-by: Leonardo de Moura --- tests/lean/run/class_coe.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean index 0fd7b20589..7feae75afa 100644 --- a/tests/lean/run/class_coe.lean +++ b/tests/lean/run/class_coe.lean @@ -46,8 +46,10 @@ check 0 + i check i + 0 check 0 + x check x + 0 +namespace foo variable eq {A : Type} : A → A → Prop infixl `=`:50 := eq abbreviation id (A : Type) (a : A) := a notation A `=` B `:` C := @eq C A B check nat_to_int n + nat_to_int m = (n + m) : int +end foo