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

feat(lua): add Type function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-08 15:52:58 -08:00
parent 32605d8266
commit 5a97f730af
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "library/expr_lt.h"
#include "bindings/lua/util.h"
#include "bindings/lua/name.h"
#include "bindings/lua/level.h"
namespace lean {
constexpr char const * expr_mt = "expr.mt";
@ -157,6 +158,14 @@ static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L, "fun"); }
static int expr_pi(lua_State * L) { return expr_abst<Pi, Pi>(L, "Pi"); }
static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L, "Let"); }
static int expr_type(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 0)
return push_expr(L, Type());
else
return push_expr(L, Type(to_level(L, 1)));
}
static const struct luaL_Reg expr_m[] = {
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
@ -186,5 +195,7 @@ void open_expr(lua_State * L) {
set_global_function<expr_fun>(L, "Fun");
set_global_function<expr_pi>(L, "Pi");
set_global_function<expr_let>(L, "Let");
set_global_function<expr_type>(L, "mk_type");
set_global_function<expr_type>(L, "Type");
}
}

4
tests/lua/expr3.lua Normal file
View file

@ -0,0 +1,4 @@
t = Type()
print(t)
t = Type(level("U"))
print(t)