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

fix(lua): typos and a bug in the expr Lua bindings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-11 13:11:06 -08:00
parent b227775a07
commit 8dd85ebc15
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/bindings/lua/expr.cpp
View file

@ -32,7 +32,7 @@ expr & to_expr(lua_State * L, int idx) {
expr & to_nonnull_expr(lua_State * L, int idx) { expr & to_nonnull_expr(lua_State * L, int idx) {
expr & r = to_expr(L, idx); expr & r = to_expr(L, idx);
if (!r) if (!r)
luaL_error(L, "non null Lean expression expected"); luaL_error(L, "non-null Lean expression expected");
return r; return r;
} }
@ -99,7 +99,7 @@ static int expr_mk_lambda(lua_State * L) {
} }
static int expr_mk_pi(lua_State * L) { static int expr_mk_pi(lua_State * L) {
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); return push_expr(L, mk_pi(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
} }
static int expr_mk_let(lua_State * L) { static int expr_mk_let(lua_State * L) {
@ -146,7 +146,7 @@ int expr_abst(lua_State * L, char const * fname) {
luaL_error(L, "Lean %s expects arg #1 to be of the form '{{expr, expr}, ...}'", fname); luaL_error(L, "Lean %s expects arg #1 to be of the form '{{expr, expr}, ...}'", fname);
int len = objlen(L, 1); int len = objlen(L, 1);
if (len == 0) if (len == 0)
luaL_error(L, "Lean %s expects arg #1 to be non-empty table", fname); luaL_error(L, "Lean %s expects arg #1 to be a non-empty table", fname);
expr r = to_nonnull_expr(L, 2); expr r = to_nonnull_expr(L, 2);
for (int i = len; i >= 1; i--) { for (int i = len; i >= 1; i--) {
auto p = get_expr_pair_from_table(L, 1, i); auto p = get_expr_pair_from_table(L, 1, i);