max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: integer type in llvm_count_params

Browse source
This commit is contained in:
Sebastian Ullrich 2023-08-18 18:22:48 +02:00
parent 4e52283728
commit 63d2bdd490
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/llvm.cpp
View file

@ -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
}