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