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

test(kernel/expr): check if the serializer works for metavariables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-15 17:15:56 -08:00
parent 5058e403b5
commit 438fa8251b
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/tests/kernel/expr.cpp
View file

@ -402,6 +402,16 @@ static void tst20() {
check_serializer(t);
}
static void tst21() {
local_context lctx;
lctx = cons(mk_lift(1, 2), lctx);
lctx = cons(mk_inst(1, Const("a")), lctx);
lctx = cons(mk_lift(0, 1), lctx);
expr m = mk_metavar("m1", lctx);
expr t = Const("f")(m, m, mk_metavar("m2"));
check_serializer(t);
}
int main() {
save_stack_info();
lean_assert(sizeof(expr) == sizeof(optional<expr>));
@ -425,6 +435,7 @@ int main() {
tst18();
tst19();
tst20();
tst21();
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";