From 64c3be44f86573e2d4ea74459c0f0df41eaa0346 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Apr 2020 18:23:45 -0700 Subject: [PATCH] fix: `lean_unbox_float` --- src/runtime/lean.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/runtime/lean.h b/src/runtime/lean.h index acb8a3eeda..b19733c0db 100644 --- a/src/runtime/lean.h +++ b/src/runtime/lean.h @@ -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); }