From 3c4b3c1ad6fbbdd909c8e301cf182810e77c8b63 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 23 Aug 2015 19:55:45 -0700
Subject: [PATCH] test(tests/shared/env): add total order simple tests

---
 src/tests/shared/env.c | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/tests/shared/env.c b/src/tests/shared/env.c
index a2f414673..7a34089cd 100644
--- a/src/tests/shared/env.c
+++ b/src/tests/shared/env.c
@@ -192,6 +192,10 @@ void test_id() {
     lean_cert_decl id_cert_def;
     lean_env new_env;
     lean_univ zero, one;
+    lean_bool is_lt;
+
+    check(lean_expr_lt(f, id_val, &is_lt, &ex) && is_lt);
+    check(lean_expr_lt(id_val, f, &is_lt, &ex) && !is_lt);
 
     printf("id type:  ");
     print_expr(id_type);
@@ -210,6 +214,8 @@ void test_id() {
 
     check(lean_univ_mk_zero(&zero, &ex));
     check(lean_univ_mk_succ(zero, &one, &ex));
+    check(lean_univ_lt(zero, one, &is_lt, &ex) && is_lt);
+    check(lean_univ_lt(one, zero, &is_lt, &ex) && !is_lt);
     {
         lean_type_checker tc;
         lean_expr T0  = mk_sort(zero);