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

feat(library/kernel_bindings): make mk_arrow nary in the Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 09:37:50 -07:00
parent 08ac9c1f05
commit 6f8f074f20
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/kernel_bindings.cpp
View file

@ -279,7 +279,15 @@ static int expr_mk_pi(lua_State * L) {
else
return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr_binder_info(L, 4)));
}
static int expr_mk_arrow(lua_State * L) { return push_expr(L, mk_arrow(to_expr(L, 1), to_expr(L, 2))); }
static int expr_mk_arrow(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs < 2)
throw exception("function must have at least 2 arguments");
expr r = mk_arrow(to_expr(L, nargs - 1), to_expr(L, nargs));
for (int i = nargs - 2; i >= 1; i--)
r = mk_arrow(to_expr(L, i), r);
return push_expr(L, r);
}
static int expr_mk_let(lua_State * L) { return push_expr(L, mk_let(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4))); }
static expr get_expr_from_table(lua_State * L, int t, int i) {