From 63d2bdd4908b4df7db381537af754a7319e334e4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 18 Aug 2023 18:22:48 +0200 Subject: [PATCH] fix: integer type in `llvm_count_params` --- src/library/compiler/llvm.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp index 428f6634fc..2b15190a06 100644 --- a/src/library/compiler/llvm.cpp +++ b/src/library/compiler/llvm.cpp @@ -1022,7 +1022,7 @@ extern "C" LEAN_EXPORT lean_object * llvm_count_params(size_t ctx, size_t f, false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " "the LLVM backend function.")); #else - int n = LLVMCountParams(lean_to_Value(f)); + unsigned n = LLVMCountParams(lean_to_Value(f)); return lean_io_result_mk_ok(lean_box_uint64(n)); #endif // LEAN_LLVM }