lean2/src/util/numerics/open_module.h

/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#pragma once
#include "util/numerics/mpz.h"
#include "util/numerics/mpq.h"

namespace lean {
inline void open_numerics_module(lua_State * L) {
    open_mpz(L);
    open_mpq(L);
}
}
feat(lua): expose basic API for Lean expressions in the Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-08 05:53:57 +00:00			`/*`
			`Copyright (c) 2013 Microsoft Corporation. All rights reserved.`
			`Released under Apache 2.0 license as described in the file LICENSE.`

			`Author: Leonardo de Moura`
			`*/`
refactor(lua): remove duplicate code, separate lua_exception, add missing #pragma once Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-08 19:59:47 +00:00			`#pragma once`
refactor(bindings/lua): move Lua bindings to the file associated with them The directory bindings/lua was getting too big and had too many dependencies. Moreover, it was getting too painful to edit/maintain two different places. Now, the bindings for module X are in the directory that defines X. For example, the bindings for util/name.cpp are located at util/name.cpp. The only exception is the kernel. We do not want to inflate the kernel with Lua bindings. The bindings for the kernel classes are located at bindings/kernel_bindings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-27 03:15:49 +00:00			`#include "util/numerics/mpz.h"`
			`#include "util/numerics/mpq.h"`

feat(lua): expose basic API for Lean expressions in the Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-08 05:53:57 +00:00			`namespace lean {`
refactor(bindings/lua): move Lua bindings to the file associated with them The directory bindings/lua was getting too big and had too many dependencies. Moreover, it was getting too painful to edit/maintain two different places. Now, the bindings for module X are in the directory that defines X. For example, the bindings for util/name.cpp are located at util/name.cpp. The only exception is the kernel. We do not want to inflate the kernel with Lua bindings. The bindings for the kernel classes are located at bindings/kernel_bindings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-27 03:15:49 +00:00			`inline void open_numerics_module(lua_State * L) {`
			`open_mpz(L);`
			`open_mpq(L);`
			`}`
feat(lua): expose basic API for Lean expressions in the Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-11-08 05:53:57 +00:00			`}`