From 243f80231ac2d6cb0a3aa8b809ecb5e86537ff7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Sep 2014 18:25:15 -0700 Subject: [PATCH] chore(kernel): fix style and lua bindings --- src/kernel/environment.h | 2 +- src/library/kernel_bindings.cpp | 2 +- tests/lua/env5.lua | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 39678fe1f3..9a86b45170 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -29,7 +29,7 @@ class type_checker; class environment; class certified_declaration; -typedef std::function extra_opaque_pred; +typedef std::function extra_opaque_pred; // NOLINT extra_opaque_pred const & no_extra_opaque(); /** diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 2b9166e34d..d94ab9a900 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1842,8 +1842,8 @@ static int mk_type_checker(lua_State * L) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); } else { optional mod_idx; bool memoize; name_set extra_opaque; - extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque); + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), mk_default_converter(to_environment(L, 1), mod_idx, memoize, pred), memoize); diff --git a/tests/lua/env5.lua b/tests/lua/env5.lua index 75746d8d14..e2e9ef9223 100644 --- a/tests/lua/env5.lua +++ b/tests/lua/env5.lua @@ -56,5 +56,6 @@ assert(not pcall(function() print(tc2:check(id_1(Type, a))) end)) assert(tc2:whnf(id_2(Type, a)) == a) assert(tc2:whnf(id_2(Type, id_2(Type, a))) == a) local tc3 = type_checker(env, name_generator("foo"), {extra_opaque=name_set("id")}) +print(tc3:whnf(id_2(Type, id_2(Type, a)))) assert(tc3:whnf(id_2(Type, id_2(Type, a))) == id_2(Type, id_2(Type, a))) print(id_2(Type, id_2(Type, a)))