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