Zulip Chat Archive
Stream: lean4
Topic: leanc incompatible pointer error
Trebor Huang (Jan 09 2024 at 12:53):
I'm using nightly-2024-01-09.
def foo (n m : Nat) (h : False) : Nat :=
if n < m then
h.elim
else
n - m
def main : IO Unit :=
IO.println s!"Hello! {foo 3 2 sorry}"
Produces an error when compiled:
error: > /[...]/.elan/toolchains/leanprover--lean4---nightly-2024-01-09/bin/leanc -c -o ./.lake/build/ir/Main.c.o ./.lake/build/ir/Main.c -O3 -DNDEBUG
error: stderr:
./.lake/build/ir/Main.c:55:23: error: incompatible pointer to integer conversion passing 'lean_object *' to parameter of type 'uint8_t' (aka 'unsigned char') [-Wint-conversion]
x_3 = l_foo(x_1, x_2, lean_box(0));
^~~~~~~~~~~
./.lake/build/ir/Main.c:29:76: note: passing argument to parameter 'x_3' here
LEAN_EXPORT lean_object* l_foo(lean_object* x_1, lean_object* x_2, uint8_t x_3) {
^
1 error generated.
error: external command `/[...]/.elan/toolchains/leanprover--lean4---nightly-2024-01-09/bin/leanc` exited with code 1
Last updated: May 02 2025 at 03:31 UTC