From d6b4b96ab803e596afee465d99e12e25a4eaefc6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2019 18:09:23 -0800 Subject: [PATCH] test: `HasBeq Nat` instance --- tests/lean/run/frontend1.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index 5e48c348ea..4ab4ce0e5c 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -27,6 +27,7 @@ pure "hello" #eval run "#check HasAdd.add one two" #eval run "#check one + two > one ∧ True" #eval run "#check act1 >>= IO.println" +#eval run "#check one + two == one" #eval run "universe u universe v