michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/shared/env): add total order simple tests

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-23 19:55:45 -07:00
parent 78e9a57e06
commit 3c4b3c1ad6
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tests/shared/env.c
View file

@ -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);