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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2020-04-03 17:48:06 -07:00
parent d1b0bd0c77
commit 8e952f3c36
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/runtime/lean.h
View file

@ -1672,7 +1672,7 @@ static inline size_t lean_unbox_usize(b_lean_obj_arg o) {
}
static inline lean_obj_res lean_box_float(double v) {
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double));
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double)); // NOLINT
lean_ctor_set_float(r, 0, v);
return r;
}

2
src/runtime/object.cpp
View file

@ -1451,7 +1451,7 @@ extern "C" usize lean_usize_mix_hash(usize a1, usize a2) {
extern "C" double lean_float_of_nat(b_lean_obj_arg a) {
if (lean_is_scalar(a)) {
return (double)lean_unbox(a);
return static_cast<double>(lean_unbox(a));
} else {
return std::nan(""); // TODO(Leo): improve
}