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

fix: lean_unbox_float

Browse source
This commit is contained in:
Leonardo de Moura 2020-04-03 18:23:45 -07:00
parent 8e952f3c36
commit 64c3be44f8
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/runtime/lean.h
View file

@ -1677,7 +1677,7 @@ static inline lean_obj_res lean_box_float(double v) {
return r;
}
static inline uint64_t lean_unbox_float(b_lean_obj_arg o) {
static inline double lean_unbox_float(b_lean_obj_arg o) {
return lean_ctor_get_float(o, 0);
}