summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/CWayland/CWayland.c6
-rw-r--r--lib/Wayland.lean1
-rw-r--r--lib/Wayland/Native.lean2
3 files changed, 9 insertions, 0 deletions
diff --git a/lib/CWayland/CWayland.c b/lib/CWayland/CWayland.c
new file mode 100644
index 0000000..2b9bf6d
--- /dev/null
+++ b/lib/CWayland/CWayland.c
@@ -0,0 +1,6 @@
+#include <lean/lean.h>
+
+lean_obj_res lean_test_answer()
+{
+ return lean_io_result_mk_ok(lean_int_to_int(42));
+} \ No newline at end of file
diff --git a/lib/Wayland.lean b/lib/Wayland.lean
new file mode 100644
index 0000000..16f5c4c
--- /dev/null
+++ b/lib/Wayland.lean
@@ -0,0 +1 @@
+import Wayland.Native
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
new file mode 100644
index 0000000..ded2e3a
--- /dev/null
+++ b/lib/Wayland/Native.lean
@@ -0,0 +1,2 @@
+@[extern "lean_test_answer"]
+opaque testAnswer : IO Int