diff --git a/stage0/src/Init/Data.lean b/stage0/src/Init/Data.lean
index 11dc7139ac..273b7e21b3 100644
--- a/stage0/src/Init/Data.lean
+++ b/stage0/src/Init/Data.lean
@@ -14,6 +14,7 @@ import Init.Data.Array
 import Init.Data.ByteArray
 import Init.Data.Fin
 import Init.Data.UInt
+import Init.Data.Float
 import Init.Data.RBTree
 import Init.Data.RBMap
 import Init.Data.Option
diff --git a/stage0/src/Init/Data/Float.lean b/stage0/src/Init/Data/Float.lean
new file mode 100644
index 0000000000..c946cad305
--- /dev/null
+++ b/stage0/src/Init/Data/Float.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+import Init.Data.ToString
+
+structure FloatSpec :=
+(float : Type)
+(val   : float)
+(lt    : float → float → Prop)
+(le    : float → float → Prop)
+(decEq : DecidableEq float)
+(decLt : DecidableRel lt)
+(decLe : DecidableRel le)
+
+-- Just show FloatSpec is inhabited.
+constant floatSpec : FloatSpec := {
+  float := Unit,
+  val   := (),
+  lt    := fun _ _ => True,
+  le    := fun _ _ => True,
+  decEq := inferInstanceAs (DecidableEq Unit),
+  decLt := fun _ _ => inferInstanceAs (Decidable True),
+  decLe := fun _ _ => inferInstanceAs (Decidable True)
+}
+
+def Float : Type := floatSpec.float
+instance : Inhabited Float := ⟨floatSpec.val⟩
+
+/- @[extern "lean_float_of_nat"] -/ constant Float.ofNat : (@& Nat) → Float := arbitrary _
+/- @[extern c inline "#1 + #2"] -/  constant Float.add : Float → Float → Float := arbitrary _
+/- @[extern c inline "#1 - #2"] -/  constant Float.sub : Float → Float → Float := arbitrary _
+/- @[extern c inline "#1 * #2"] -/  constant Float.mul : Float → Float → Float := arbitrary _
+/- @[extern c inline "#1 / #2"] -/  constant Float.div : Float → Float → Float := arbitrary _
+
+def Float.lt  : Float → Float → Prop := floatSpec.lt
+def Float.le  : Float → Float → Prop := floatSpec.le
+
+instance : HasZero Float   := ⟨Float.ofNat 0⟩
+instance : HasOne Float    := ⟨Float.ofNat 1⟩
+instance : HasOfNat Float  := ⟨Float.ofNat⟩
+instance : HasAdd Float    := ⟨Float.add⟩
+instance : HasSub Float    := ⟨Float.sub⟩
+instance : HasMul Float    := ⟨Float.mul⟩
+instance : HasDiv Float    := ⟨Float.div⟩
+instance : HasLess Float   := ⟨Float.lt⟩
+instance : HasLessEq Float := ⟨Float.le⟩
+
+/- @[extern c inline "#1 == #2"] -/ constant Float.decEq (a b : Float) : Decidable (a = b) := floatSpec.decEq a b
+/- @[extern c inline "#1 < #2"]  -/  constant Float.decLt (a b : Float) : Decidable (a < b) := floatSpec.decLt a b
+/- @[extern c inline "#1 <= #2"] -/ constant Float.decLe (a b : Float) : Decidable (a ≤ b) := floatSpec.decLe a b
+
+/- @[extern "lean_float_to_string"] -/ constant Float.toString : Float → String := arbitrary _
+
+instance : HasToString Float := ⟨Float.toString⟩
diff --git a/stage0/src/Init/Lean/Compiler/IR/EmitC.lean b/stage0/src/Init/Lean/Compiler/IR/EmitC.lean
index b73803fbb3..1523dd3012 100644
--- a/stage0/src/Init/Lean/Compiler/IR/EmitC.lean
+++ b/stage0/src/Init/Lean/Compiler/IR/EmitC.lean
@@ -311,7 +311,7 @@ emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitL
 
 def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit := do
 match t with
-| IRType.float  => throw "floats are not supported yet"
+| IRType.float  => emit "lean_ctor_set_float"
 | IRType.uint8  => emit "lean_ctor_set_uint8"
 | IRType.uint16 => emit "lean_ctor_set_uint16"
 | IRType.uint32 => emit "lean_ctor_set_uint32"
@@ -386,7 +386,7 @@ emitLhs z; emit "lean_ctor_get_usize("; emit x; emit ", "; emit i; emitLn ");"
 def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit := do
 emitLhs z;
 match t with
-| IRType.float  => throw "floats are not supported yet"
+| IRType.float  => emit "lean_ctor_get_float"
 | IRType.uint8  => emit "lean_ctor_get_uint8"
 | IRType.uint16 => emit "lean_ctor_get_uint16"
 | IRType.uint32 => emit "lean_ctor_get_uint32"
@@ -447,7 +447,7 @@ match xType with
 | IRType.usize  => emit "lean_box_usize"
 | IRType.uint32 => emit "lean_box_uint32"
 | IRType.uint64 => emit "lean_box_uint64"
-| IRType.float  => throw "floats are not supported yet"
+| IRType.float  => emit "lean_box_float"
 | other         => emit "lean_box"
 
 def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do
@@ -459,7 +459,7 @@ match t with
 | IRType.usize  => emit "lean_unbox_usize"
 | IRType.uint32 => emit "lean_unbox_uint32"
 | IRType.uint64 => emit "lean_unbox_uint64"
-| IRType.float  => throw "floats are not supported yet"
+| IRType.float  => emit "lean_unbox_float"
 | other         => emit "lean_unbox";
 emit "("; emit x; emitLn ");"
 
diff --git a/stage0/src/library/compiler/ir.cpp b/stage0/src/library/compiler/ir.cpp
index bd8192f009..73c154e80c 100644
--- a/stage0/src/library/compiler/ir.cpp
+++ b/stage0/src/library/compiler/ir.cpp
@@ -117,8 +117,10 @@ static ir::type to_ir_type(expr const & e) {
             return ir::type::UInt64;
         } else if (const_name(e) == get_usize_name()) {
             return ir::type::USize;
+        } else if (const_name(e) == get_float_name()) {
+            return ir::type::Float;
         }
-    } else if (is_pi(e)) {
+     } else if (is_pi(e)) {
         return ir::type::Object;
     }
     throw exception("IR unsupported type");
@@ -334,6 +336,16 @@ class to_ir_fn {
         return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), size_to_ir_type(sz), b);
     }
 
+    ir::fn_body visit_fset(local_decl const & decl, ir::fn_body const & b) {
+        expr val = *decl.get_value();
+        buffer<expr> args;
+        expr const & fn = get_app_args(val, args);
+        lean_assert(args.size() == 2);
+        unsigned n, offset;
+        lean_verify(is_llnf_fset(fn, n, offset));
+        return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float, b);
+    }
+
     ir::fn_body visit_uset(local_decl const & decl, ir::fn_body const & b) {
         expr val = *decl.get_value();
         buffer<expr> args;
@@ -360,6 +372,14 @@ class to_ir_fn {
         return mk_vdecl(decl, v, b);
     }
 
+    ir::fn_body visit_fproj(local_decl const & decl, ir::fn_body const & b) {
+        expr val = *decl.get_value();
+        unsigned n, offset;
+        lean_verify(is_llnf_fproj(get_app_fn(val), n, offset));
+        ir::expr v = ir::mk_sproj(n, offset, to_var_id(app_arg(val)));
+        return mk_vdecl(decl, v, b);
+    }
+
     ir::fn_body visit_uproj(local_decl const & decl, ir::fn_body const & b) {
         expr val = *decl.get_value();
         unsigned n;
@@ -391,12 +411,16 @@ class to_ir_fn {
                 return visit_papp(decl, b);
             else if (is_llnf_sset(fn))
                 return visit_sset(decl, b);
+            else if (is_llnf_fset(fn))
+                return visit_fset(decl, b);
             else if (is_llnf_uset(fn))
                 return visit_uset(decl, b);
             else if (is_llnf_proj(fn))
                 return visit_proj(decl, b);
             else if (is_llnf_sproj(fn))
                 return visit_sproj(decl, b);
+            else if (is_llnf_fproj(fn))
+                return visit_fproj(decl, b);
             else if (is_llnf_uproj(fn))
                 return visit_uproj(decl, b);
             else if (is_constant(fn))
diff --git a/stage0/src/library/compiler/llnf.cpp b/stage0/src/library/compiler/llnf.cpp
index 7cec77a69e..b5b438663b 100644
--- a/stage0/src/library/compiler/llnf.cpp
+++ b/stage0/src/library/compiler/llnf.cpp
@@ -32,10 +32,12 @@ static expr * g_closure     = nullptr;
 static char const * g_cnstr = "_cnstr";
 static name * g_reuse       = nullptr;
 static name * g_reset       = nullptr;
+static name * g_fset        = nullptr;
 static name * g_sset        = nullptr;
 static name * g_uset        = nullptr;
 static name * g_proj        = nullptr;
 static name * g_sproj       = nullptr;
+static name * g_fproj       = nullptr;
 static name * g_uproj       = nullptr;
 static expr * g_jmp         = nullptr;
 static name * g_box         = nullptr;
@@ -57,6 +59,17 @@ static bool is_llnf_unary_primitive(expr const & e, name const & prefix, unsigne
     return true;
 }
 
+static bool is_llnf_binary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2) {
+    if (!is_constant(e)) return false;
+    name const & n2 = const_name(e);
+    if (n2.is_atomic() || !n2.is_numeral()) return false;
+    i2 = n2.get_numeral().get_small_value();
+    name const & n1 = n2.get_prefix();
+    if (n1.is_atomic() || !n1.is_numeral() || n1.get_prefix() != prefix) return false;
+    i1 = n1.get_numeral().get_small_value();
+    return true;
+}
+
 static bool is_llnf_ternary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2, unsigned & i3) {
     if (!is_constant(e)) return false;
     name const & n3  = const_name(e);
@@ -145,6 +158,9 @@ bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitiv
 expr mk_llnf_sset(unsigned sz, unsigned n, unsigned offset) { return mk_constant(name(name(name(*g_sset, sz), n), offset)); }
 bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset) { return is_llnf_ternary_primitive(e, *g_sset, sz, n, offset); }
 
+expr mk_llnf_fset(unsigned n, unsigned offset) { return mk_constant(name(name(*g_fset, n), offset)); }
+bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fset, n, offset); }
+
 /* The `_uset.<n>` instruction sets a `usize` value in a constructor object at offset `sizeof(void*)*n`. */
 expr mk_llnf_uset(unsigned n) { return mk_constant(name(*g_uset, n)); }
 bool is_llnf_uset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_uset, n); }
@@ -157,6 +173,9 @@ bool is_llnf_proj(expr const & e, unsigned & idx) { return is_llnf_unary_primiti
 expr mk_llnf_sproj(unsigned sz, unsigned n, unsigned offset) { return mk_constant(name(name(name(*g_sproj, sz), n), offset)); }
 bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset) { return is_llnf_ternary_primitive(e, *g_sproj, sz, n, offset); }
 
+expr mk_llnf_fproj(unsigned n, unsigned offset) { return mk_constant(name(name(*g_sproj, n), offset)); }
+bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fproj, n, offset); }
+
 /* The `_uproj.<idx>` instruction retrieves an `usize` field in a constructor object at offset `sizeof(void*)*idx` */
 expr mk_llnf_uproj(unsigned idx) { return mk_constant(name(*g_uproj, idx)); }
 bool is_llnf_uproj(expr const & e, unsigned & idx) { return is_llnf_unary_primitive(e, *g_uproj, idx); }
@@ -197,9 +216,11 @@ bool is_llnf_op(expr const & e) {
         is_llnf_reuse(e)   ||
         is_llnf_reset(e)   ||
         is_llnf_sset(e)    ||
+        is_llnf_fset(e)    ||
         is_llnf_uset(e)    ||
         is_llnf_proj(e)    ||
         is_llnf_sproj(e)   ||
+        is_llnf_fproj(e)   ||
         is_llnf_uproj(e)   ||
         is_llnf_jmp(e)     ||
         is_llnf_box(e)     ||
@@ -482,6 +503,10 @@ class to_lambda_pure_fn {
         return mk_app(mk_llnf_sproj(size, num, offset), major);
     }
 
+    expr mk_fproj(expr const & major, unsigned num, unsigned offset) {
+        return mk_app(mk_llnf_fproj(num, offset), major);
+    }
+
     expr mk_uproj(expr const & major, unsigned idx) {
         return mk_app(mk_llnf_uproj(idx), major);
     }
@@ -490,6 +515,10 @@ class to_lambda_pure_fn {
         return mk_app(mk_llnf_sset(size, num, offset), major, v);
     }
 
+    expr mk_fset(expr const & major, unsigned num, unsigned offset, expr const & v) {
+        return mk_app(mk_llnf_fset(num, offset), major, v);
+    }
+
     expr mk_uset(expr const & major, unsigned idx, expr const & v) {
         return mk_app(mk_llnf_uset(idx), major, v);
     }
@@ -551,7 +580,11 @@ class to_lambda_pure_fn {
                     fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
                     break;
                 case field_info::Scalar:
-                    fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
+                    if (info.is_float()) {
+                        fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
+                    } else {
+                        fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
+                    }
                     break;
                 }
                 minor = binding_body(minor);
@@ -644,7 +677,11 @@ class to_lambda_pure_fn {
                 if (first) {
                     r = mk_let_decl(mk_enf_object_type(), r);
                 }
-                r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
+                if (info.is_float()) {
+                    r = mk_let_decl(mk_enf_object_type(), mk_fset(r, info.m_idx, info.m_offset, args[j]));
+                } else {
+                    r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
+                }
                 first = false;
                 break;
             case field_info::USize:
@@ -686,8 +723,13 @@ class to_lambda_pure_fn {
                     return mk_app(mk_llnf_uproj(info.m_idx), visit(proj_expr(e)));
                 break;
             case field_info::Scalar:
-                if (proj_idx(e) == i)
-                    return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
+                if (proj_idx(e) == i) {
+                    if (info.is_float()) {
+                        return mk_fproj(visit(proj_expr(e)), info.m_idx, info.m_offset);
+                    } else {
+                        return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
+                    }
+                }
                 break;
             }
             i++;
@@ -778,9 +820,11 @@ void initialize_llnf() {
     g_reuse     = new name("_reuse");
     g_reset     = new name("_reset");
     g_sset      = new name("_sset");
+    g_fset      = new name("_fset");
     g_uset      = new name("_uset");
     g_proj      = new name("_proj");
     g_sproj     = new name("_sproj");
+    g_fproj     = new name("_sproj");
     g_uproj     = new name("_uproj");
     g_jmp       = new expr(mk_constant("_jmp"));
     g_box       = new name("_box");
@@ -796,8 +840,10 @@ void finalize_llnf() {
     delete g_reuse;
     delete g_reset;
     delete g_sset;
+    delete g_fset;
     delete g_proj;
     delete g_sproj;
+    delete g_fproj;
     delete g_uset;
     delete g_uproj;
     delete g_jmp;
diff --git a/stage0/src/library/compiler/llnf.h b/stage0/src/library/compiler/llnf.h
index 0638eeb56b..eddd346830 100644
--- a/stage0/src/library/compiler/llnf.h
+++ b/stage0/src/library/compiler/llnf.h
@@ -22,8 +22,10 @@ bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned
 bool is_llnf_reset(expr const & e, unsigned & n);
 bool is_llnf_proj(expr const & e, unsigned & idx);
 bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
+bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uproj(expr const & e, unsigned & idx);
 bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
+bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uset(expr const & e, unsigned & n);
 bool is_llnf_jmp(expr const & e);
 bool is_llnf_unbox(expr const & e, unsigned & n);
@@ -37,8 +39,10 @@ inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2, d3; bool u; return
 inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }
 inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); }
 inline bool is_llnf_sproj(expr const & e) { unsigned d1, d2, d3; return is_llnf_sproj(e, d1, d2, d3); }
+inline bool is_llnf_fproj(expr const & e) { unsigned d1, d2; return is_llnf_fproj(e, d1, d2); }
 inline bool is_llnf_uproj(expr const & e) { unsigned d; return is_llnf_uproj(e, d); }
 inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_sset(e, d1, d2, d3); }
+inline bool is_llnf_fset(expr const & e) { unsigned d1, d2; return is_llnf_fset(e, d1, d2); }
 inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
 inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
 inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); }
@@ -61,6 +65,7 @@ struct field_info {
     field_info(unsigned sz, unsigned num, unsigned offset, expr const & type):
         m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type) {}
     expr get_type() const { return m_type; }
+    bool is_float() const { return is_constant(m_type, get_float_name()); }
     static field_info mk_irrelevant() { return field_info(); }
     static field_info mk_object(unsigned idx) { return field_info(idx); }
     static field_info mk_usize() { return field_info(0, true); }
diff --git a/stage0/src/library/compiler/util.cpp b/stage0/src/library/compiler/util.cpp
index 95b1ff18ec..d6afe778ee 100644
--- a/stage0/src/library/compiler/util.cpp
+++ b/stage0/src/library/compiler/util.cpp
@@ -370,6 +370,7 @@ bool is_runtime_builtin_type(name const & n) {
         n == get_uint32_name() ||
         n == get_uint64_name() ||
         n == get_usize_name()  ||
+        n == get_float_name()  ||
         n == get_thunk_name()  ||
         n == get_task_name()   ||
         n == get_array_name()  ||
@@ -385,7 +386,8 @@ bool is_runtime_scalar_type(name const & n) {
         n == get_uint16_name() ||
         n == get_uint32_name() ||
         n == get_uint64_name() ||
-        n == get_usize_name();
+        n == get_usize_name()  ||
+        n == get_float_name();
 }
 
 bool is_llnf_unboxed_type(expr const & type) {
@@ -758,6 +760,7 @@ void initialize_compiler_util() {
     g_builtin_scalar_size->emplace_back(get_uint16_name(), 2);
     g_builtin_scalar_size->emplace_back(get_uint32_name(), 4);
     g_builtin_scalar_size->emplace_back(get_uint64_name(), 8);
+    g_builtin_scalar_size->emplace_back(get_float_name(),  8);
 }
 
 void finalize_compiler_util() {
diff --git a/stage0/src/library/constants.cpp b/stage0/src/library/constants.cpp
index 36868343ae..5d259a734d 100644
--- a/stage0/src/library/constants.cpp
+++ b/stage0/src/library/constants.cpp
@@ -57,6 +57,7 @@ name const * g_eq_of_heq = nullptr;
 name const * g_eq_true_intro = nullptr;
 name const * g_eq_false_intro = nullptr;
 name const * g_eq_self_iff_true = nullptr;
+name const * g_float = nullptr;
 name const * g_lean_message_data = nullptr;
 name const * g_lean_monad_tracer_trace = nullptr;
 name const * g_false = nullptr;
@@ -247,6 +248,7 @@ void initialize_constants() {
     g_eq_true_intro = new name{"eqTrueIntro"};
     g_eq_false_intro = new name{"eqFalseIntro"};
     g_eq_self_iff_true = new name{"eqSelfIffTrue"};
+    g_float = new name{"Float"};
     g_lean_message_data = new name{"Lean", "MessageData"};
     g_lean_monad_tracer_trace = new name{"Lean", "MonadTracer", "trace"};
     g_false = new name{"False"};
@@ -438,6 +440,7 @@ void finalize_constants() {
     delete g_eq_true_intro;
     delete g_eq_false_intro;
     delete g_eq_self_iff_true;
+    delete g_float;
     delete g_lean_message_data;
     delete g_lean_monad_tracer_trace;
     delete g_false;
@@ -628,6 +631,7 @@ name const & get_eq_of_heq_name() { return *g_eq_of_heq; }
 name const & get_eq_true_intro_name() { return *g_eq_true_intro; }
 name const & get_eq_false_intro_name() { return *g_eq_false_intro; }
 name const & get_eq_self_iff_true_name() { return *g_eq_self_iff_true; }
+name const & get_float_name() { return *g_float; }
 name const & get_lean_message_data_name() { return *g_lean_message_data; }
 name const & get_lean_monad_tracer_trace_name() { return *g_lean_monad_tracer_trace; }
 name const & get_false_name() { return *g_false; }
diff --git a/stage0/src/library/constants.h b/stage0/src/library/constants.h
index 6f8a9bc49f..8088d71708 100644
--- a/stage0/src/library/constants.h
+++ b/stage0/src/library/constants.h
@@ -59,6 +59,7 @@ name const & get_eq_of_heq_name();
 name const & get_eq_true_intro_name();
 name const & get_eq_false_intro_name();
 name const & get_eq_self_iff_true_name();
+name const & get_float_name();
 name const & get_lean_message_data_name();
 name const & get_lean_monad_tracer_trace_name();
 name const & get_false_name();
diff --git a/stage0/src/library/constants.txt b/stage0/src/library/constants.txt
index ed814182d5..f9867d873e 100644
--- a/stage0/src/library/constants.txt
+++ b/stage0/src/library/constants.txt
@@ -52,6 +52,7 @@ eqOfHEq
 eqTrueIntro
 eqFalseIntro
 eqSelfIffTrue
+Float
 Lean.MessageData
 Lean.MonadTracer.trace
 False
diff --git a/stage0/src/runtime/lean.h b/stage0/src/runtime/lean.h
index 8583217d6e..f8db550364 100644
--- a/stage0/src/runtime/lean.h
+++ b/stage0/src/runtime/lean.h
@@ -703,6 +703,11 @@ static inline uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset) {
     return *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
 }
 
+static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) {
+    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
+    return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
+}
+
 static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) {
     assert(i >= lean_ctor_num_objs(o));
     *((size_t*)(lean_ctor_obj_cptr(o) + i)) = v;
@@ -728,6 +733,11 @@ static inline void lean_ctor_set_uint64(b_lean_obj_arg o, unsigned offset, uint6
     *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
 }
 
+static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double v) {
+    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
+    *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
+}
+
 /* Closures */
 
 static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; }
@@ -1612,6 +1622,11 @@ static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2;
 static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
 size_t lean_usize_mix_hash(size_t a1, size_t a2);
 
+/* Float */
+
+double lean_float_of_nat(b_lean_obj_arg a);
+lean_obj_res lean_float_to_string(double a);
+
 /* Boxing primitives */
 
 static inline lean_obj_res lean_box_uint32(uint32_t v) {
@@ -1656,6 +1671,16 @@ static inline size_t lean_unbox_usize(b_lean_obj_arg o) {
     return lean_ctor_get_usize(o, 0);
 }
 
+static inline lean_obj_res lean_box_float(double v) {
+    lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double));
+    lean_ctor_set_float(r, 0, v);
+    return r;
+}
+
+static inline uint64_t lean_unbox_float(b_lean_obj_arg o) {
+    return lean_ctor_get_float(o, 0);
+}
+
 /* Debugging helper functions */
 
 lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
diff --git a/stage0/src/runtime/object.cpp b/stage0/src/runtime/object.cpp
index 8fcb23f449..7c575c2d96 100644
--- a/stage0/src/runtime/object.cpp
+++ b/stage0/src/runtime/object.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <deque>
+#include <cmath>
 #include "runtime/object.h"
 #include "runtime/thread.h"
 #include "runtime/utf8.h"
@@ -1445,6 +1446,22 @@ extern "C" usize lean_usize_mix_hash(usize a1, usize a2) {
         return hash(static_cast<uint32>(a1), static_cast<uint32>(a2));
 }
 
+// =======================================
+// Float
+
+extern "C" double lean_float_of_nat(b_lean_obj_arg a) {
+    if (lean_is_scalar(a)) {
+        return (double)lean_unbox(a);
+    } else {
+        return std::nan(""); // TODO(Leo): improve
+    }
+}
+
+lean_obj_res lean_float_to_string(double a) {
+    return mk_string(std::to_string(a));
+}
+
+
 // =======================================
 // Strings
 
diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt
index 79effbc71e..a391e356b2 100644
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
@@ -1 +1 @@
-add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/String/Extra.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Delaborator.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Tactic/Generalize.c Init/./Lean/Elab/Tactic/Induction.c Init/./Lean/Elab/Tactic/Injection.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/KeyedDeclsAttribute.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/GeneralizeTelescope.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Cases.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Induction.c Init/./Lean/Meta/Tactic/Injection.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/Closure.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/FoldConsts.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/Recognizers.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./ShareCommon.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)
+add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/Float.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/String/Extra.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Delaborator.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Tactic/Generalize.c Init/./Lean/Elab/Tactic/Induction.c Init/./Lean/Elab/Tactic/Injection.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/KeyedDeclsAttribute.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/GeneralizeTelescope.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Cases.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Induction.c Init/./Lean/Meta/Tactic/Injection.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/Closure.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/FoldConsts.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/Recognizers.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./ShareCommon.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)
diff --git a/stage0/stdlib/Init/Data.c b/stage0/stdlib/Init/Data.c
index 23bfce7eb5..4ee549df21 100644
--- a/stage0/stdlib/Init/Data.c
+++ b/stage0/stdlib/Init/Data.c
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Init.Data
-// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.Fin Init.Data.UInt Init.Data.RBTree Init.Data.RBMap Init.Data.Option Init.Data.HashMap Init.Data.Random Init.Data.Queue Init.Data.Stack
+// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.RBTree Init.Data.RBMap Init.Data.Option Init.Data.HashMap Init.Data.Random Init.Data.Queue Init.Data.Stack
 #include "runtime/lean.h"
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -23,6 +23,7 @@ lean_object* initialize_Init_Data_Array(lean_object*);
 lean_object* initialize_Init_Data_ByteArray(lean_object*);
 lean_object* initialize_Init_Data_Fin(lean_object*);
 lean_object* initialize_Init_Data_UInt(lean_object*);
+lean_object* initialize_Init_Data_Float(lean_object*);
 lean_object* initialize_Init_Data_RBTree(lean_object*);
 lean_object* initialize_Init_Data_RBMap(lean_object*);
 lean_object* initialize_Init_Data_Option(lean_object*);
@@ -65,6 +66,9 @@ lean_dec_ref(res);
 res = initialize_Init_Data_UInt(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Init_Data_Float(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Init_Data_RBTree(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
diff --git a/stage0/stdlib/Init/Data/Float.c b/stage0/stdlib/Init/Data/Float.c
new file mode 100644
index 0000000000..638e1558e4
--- /dev/null
+++ b/stage0/stdlib/Init/Data/Float.c
@@ -0,0 +1,496 @@
+// Lean compiler output
+// Module: Init.Data.Float
+// Imports: Init.Core Init.Data.ToString
+#include "runtime/lean.h"
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+uint8_t l_floatSpec___elambda__1(lean_object*, lean_object*);
+lean_object* l_Float_ofNat(lean_object*);
+lean_object* l_Float_HasDiv___closed__1;
+lean_object* l_Float_HasLessEq;
+lean_object* l_Float_HasOne;
+extern lean_object* l_String_splitAux___main___closed__1;
+lean_object* l_Float_div___boxed(lean_object*, lean_object*);
+uint8_t l_Float_decEq(lean_object*, lean_object*);
+lean_object* l_floatSpec___closed__1;
+uint8_t l_Float_decLe(lean_object*, lean_object*);
+lean_object* l_floatSpec___closed__2;
+lean_object* l_Float_HasMul;
+lean_object* l_Float_HasAdd;
+lean_object* l_Float_Inhabited;
+lean_object* l_Float_HasOfNat;
+lean_object* l_Float_HasToString;
+uint8_t l_Float_decLt(lean_object*, lean_object*);
+uint8_t l_floatSpec___elambda__2(lean_object*, lean_object*);
+lean_object* l_floatSpec___elambda__2___boxed(lean_object*, lean_object*);
+extern uint8_t l_True_Decidable;
+lean_object* l_Float_mul___boxed(lean_object*, lean_object*);
+lean_object* l_Float_ofNat___boxed(lean_object*);
+lean_object* l_Float_toString(lean_object*);
+lean_object* l_Float_div(lean_object*, lean_object*);
+lean_object* l_Float_HasOfNat___closed__1;
+lean_object* l_Float_decLt___boxed(lean_object*, lean_object*);
+lean_object* l_Float_sub(lean_object*, lean_object*);
+lean_object* l_floatSpec___elambda__1___boxed(lean_object*, lean_object*);
+lean_object* l_Float_add(lean_object*, lean_object*);
+lean_object* l_floatSpec___closed__3;
+lean_object* l_Float_HasToString___closed__1;
+lean_object* l_Float_HasSub;
+lean_object* l_Float_HasSub___closed__1;
+lean_object* l_Float_HasLess;
+lean_object* l_Float_HasDiv;
+lean_object* l_Float_decLe___boxed(lean_object*, lean_object*);
+lean_object* l_Float_sub___boxed(lean_object*, lean_object*);
+lean_object* l_floatSpec;
+lean_object* l_Float_toString___boxed(lean_object*);
+lean_object* l_Float_decEq___boxed(lean_object*, lean_object*);
+lean_object* l_Float_HasAdd___closed__1;
+lean_object* l_Float_HasZero;
+lean_object* l_Float_HasMul___closed__1;
+lean_object* l_Float_add___boxed(lean_object*, lean_object*);
+lean_object* l_Float_mul(lean_object*, lean_object*);
+uint8_t l_floatSpec___elambda__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = l_True_Decidable;
+return x_3;
+}
+}
+uint8_t l_floatSpec___elambda__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = 1;
+return x_3;
+}
+}
+lean_object* _init_l_floatSpec___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_floatSpec___elambda__2___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_floatSpec___closed__2() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_floatSpec___elambda__1___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_floatSpec___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = lean_box(0);
+x_2 = l_floatSpec___closed__1;
+x_3 = l_floatSpec___closed__2;
+x_4 = lean_alloc_ctor(0, 4, 0);
+lean_ctor_set(x_4, 0, x_1);
+lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 2, x_3);
+lean_ctor_set(x_4, 3, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_floatSpec() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_floatSpec___closed__3;
+return x_1;
+}
+}
+lean_object* l_floatSpec___elambda__1___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_floatSpec___elambda__1(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_floatSpec___elambda__2___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_floatSpec___elambda__2(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Float_Inhabited() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+lean_object* l_Float_ofNat(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_box(0);
+return x_2;
+}
+}
+lean_object* l_Float_ofNat___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Float_ofNat(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Float_add(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_box(0);
+return x_3;
+}
+}
+lean_object* l_Float_add___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Float_add(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l_Float_sub(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_box(0);
+return x_3;
+}
+}
+lean_object* l_Float_sub___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Float_sub(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l_Float_mul(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_box(0);
+return x_3;
+}
+}
+lean_object* l_Float_mul___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Float_mul(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l_Float_div(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_box(0);
+return x_3;
+}
+}
+lean_object* l_Float_div___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Float_div(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* _init_l_Float_HasZero() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasOne() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasOfNat___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_ofNat___boxed), 1, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasOfNat() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasOfNat___closed__1;
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasAdd___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_add___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasAdd() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasAdd___closed__1;
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasSub___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_sub___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasSub() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasSub___closed__1;
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasMul___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_mul___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasMul() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasMul___closed__1;
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasDiv___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_div___boxed), 2, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasDiv() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasDiv___closed__1;
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasLess() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasLessEq() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
+uint8_t l_Float_decEq(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = 1;
+return x_3;
+}
+}
+lean_object* l_Float_decEq___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_Float_decEq(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+uint8_t l_Float_decLt(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = l_True_Decidable;
+return x_3;
+}
+}
+lean_object* l_Float_decLt___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_Float_decLt(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+uint8_t l_Float_decLe(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = l_True_Decidable;
+return x_3;
+}
+}
+lean_object* l_Float_decLe___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = l_Float_decLe(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_Float_toString(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_String_splitAux___main___closed__1;
+return x_2;
+}
+}
+lean_object* l_Float_toString___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Float_toString(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Float_HasToString___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_toString___boxed), 1, 0);
+return x_1;
+}
+}
+lean_object* _init_l_Float_HasToString() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Float_HasToString___closed__1;
+return x_1;
+}
+}
+lean_object* initialize_Init_Core(lean_object*);
+lean_object* initialize_Init_Data_ToString(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Init_Data_Float(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_mk_io_result(lean_box(0));
+_G_initialized = true;
+res = initialize_Init_Core(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Init_Data_ToString(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_floatSpec___closed__1 = _init_l_floatSpec___closed__1();
+lean_mark_persistent(l_floatSpec___closed__1);
+l_floatSpec___closed__2 = _init_l_floatSpec___closed__2();
+lean_mark_persistent(l_floatSpec___closed__2);
+l_floatSpec___closed__3 = _init_l_floatSpec___closed__3();
+lean_mark_persistent(l_floatSpec___closed__3);
+l_floatSpec = _init_l_floatSpec();
+lean_mark_persistent(l_floatSpec);
+l_Float_Inhabited = _init_l_Float_Inhabited();
+lean_mark_persistent(l_Float_Inhabited);
+l_Float_HasZero = _init_l_Float_HasZero();
+lean_mark_persistent(l_Float_HasZero);
+l_Float_HasOne = _init_l_Float_HasOne();
+lean_mark_persistent(l_Float_HasOne);
+l_Float_HasOfNat___closed__1 = _init_l_Float_HasOfNat___closed__1();
+lean_mark_persistent(l_Float_HasOfNat___closed__1);
+l_Float_HasOfNat = _init_l_Float_HasOfNat();
+lean_mark_persistent(l_Float_HasOfNat);
+l_Float_HasAdd___closed__1 = _init_l_Float_HasAdd___closed__1();
+lean_mark_persistent(l_Float_HasAdd___closed__1);
+l_Float_HasAdd = _init_l_Float_HasAdd();
+lean_mark_persistent(l_Float_HasAdd);
+l_Float_HasSub___closed__1 = _init_l_Float_HasSub___closed__1();
+lean_mark_persistent(l_Float_HasSub___closed__1);
+l_Float_HasSub = _init_l_Float_HasSub();
+lean_mark_persistent(l_Float_HasSub);
+l_Float_HasMul___closed__1 = _init_l_Float_HasMul___closed__1();
+lean_mark_persistent(l_Float_HasMul___closed__1);
+l_Float_HasMul = _init_l_Float_HasMul();
+lean_mark_persistent(l_Float_HasMul);
+l_Float_HasDiv___closed__1 = _init_l_Float_HasDiv___closed__1();
+lean_mark_persistent(l_Float_HasDiv___closed__1);
+l_Float_HasDiv = _init_l_Float_HasDiv();
+lean_mark_persistent(l_Float_HasDiv);
+l_Float_HasLess = _init_l_Float_HasLess();
+lean_mark_persistent(l_Float_HasLess);
+l_Float_HasLessEq = _init_l_Float_HasLessEq();
+lean_mark_persistent(l_Float_HasLessEq);
+l_Float_HasToString___closed__1 = _init_l_Float_HasToString___closed__1();
+lean_mark_persistent(l_Float_HasToString___closed__1);
+l_Float_HasToString = _init_l_Float_HasToString();
+lean_mark_persistent(l_Float_HasToString);
+return lean_mk_io_result(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif
diff --git a/stage0/stdlib/Init/Lean/Compiler/IR/EmitC.c b/stage0/stdlib/Init/Lean/Compiler/IR/EmitC.c
index 92ae10a187..20bbb8c488 100644
--- a/stage0/stdlib/Init/Lean/Compiler/IR/EmitC.c
+++ b/stage0/stdlib/Init/Lean/Compiler/IR/EmitC.c
@@ -232,6 +232,7 @@ lean_object* l_Lean_IR_EmitC_hasMainFn(lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitOffset___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*);
+lean_object* l_Lean_IR_EmitC_emitUnbox___closed__5;
 lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__23;
 lean_object* l_Lean_IR_EmitC_emitIf___closed__2;
 lean_object* l_Lean_IR_EmitC_emitArgs(lean_object*, lean_object*, lean_object*);
@@ -374,6 +375,7 @@ lean_object* l_Lean_IR_EmitC_emitMainFn___closed__37;
 lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitTailCall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitSetTag___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitMainFnIfNeeded___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_IR_EmitC_emitSProj___closed__5;
 lean_object* l_Lean_IR_EmitC_toCType___closed__11;
 lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__3;
 lean_object* l_Lean_IR_EmitC_emitReuse(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@@ -542,6 +544,7 @@ lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__20;
 lean_object* l_Lean_IR_EmitC_getEnv(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at_Lean_IR_EmitC_declareParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_getJPParams(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_EmitC_emitBoxFn___closed__5;
 lean_object* l_Lean_IR_EmitC_emitMainFn___closed__16;
 lean_object* l_Lean_IR_EmitC_emitPartialApp___closed__1;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@@ -5624,7 +5627,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSSet___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("floats are not supported yet");
+x_1 = lean_mk_string("lean_ctor_set_float");
 return x_1;
 }
 }
@@ -5676,15 +5679,10 @@ switch (lean_obj_tag(x_5)) {
 case 0:
 {
 lean_object* x_42; lean_object* x_43; 
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_2);
-lean_dec(x_1);
 x_42 = l_Lean_IR_EmitC_emitSSet___closed__1;
-x_43 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_43, 0, x_42);
-lean_ctor_set(x_43, 1, x_7);
-return x_43;
+x_43 = lean_string_append(x_7, x_42);
+x_8 = x_43;
+goto block_41;
 }
 case 1:
 {
@@ -7095,7 +7093,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_ctor_get_uint8");
+x_1 = lean_mk_string("lean_ctor_get_float");
 return x_1;
 }
 }
@@ -7103,7 +7101,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_ctor_get_uint16");
+x_1 = lean_mk_string("lean_ctor_get_uint8");
 return x_1;
 }
 }
@@ -7111,7 +7109,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_ctor_get_uint32");
+x_1 = lean_mk_string("lean_ctor_get_uint16");
 return x_1;
 }
 }
@@ -7119,6 +7117,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__4() {
 _start:
 {
 lean_object* x_1; 
+x_1 = lean_mk_string("lean_ctor_get_uint32");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__5() {
+_start:
+{
+lean_object* x_1; 
 x_1 = lean_mk_string("lean_ctor_get_uint64");
 return x_1;
 }
@@ -7131,106 +7137,87 @@ x_34 = l_Lean_IR_EmitC_emitLhs(x_1, x_6, x_7);
 switch (lean_obj_tag(x_2)) {
 case 0:
 {
-uint8_t x_35; 
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-x_35 = !lean_is_exclusive(x_34);
-if (x_35 == 0)
-{
-lean_object* x_36; lean_object* x_37; 
-x_36 = lean_ctor_get(x_34, 0);
-lean_dec(x_36);
-x_37 = l_Lean_IR_EmitC_emitSSet___closed__1;
-lean_ctor_set_tag(x_34, 1);
-lean_ctor_set(x_34, 0, x_37);
-return x_34;
+lean_object* x_35; lean_object* x_36; lean_object* x_37; 
+x_35 = lean_ctor_get(x_34, 1);
+lean_inc(x_35);
+lean_dec(x_34);
+x_36 = l_Lean_IR_EmitC_emitSProj___closed__1;
+x_37 = lean_string_append(x_35, x_36);
+x_8 = x_37;
+goto block_33;
 }
-else
+case 1:
 {
 lean_object* x_38; lean_object* x_39; lean_object* x_40; 
 x_38 = lean_ctor_get(x_34, 1);
 lean_inc(x_38);
 lean_dec(x_34);
-x_39 = l_Lean_IR_EmitC_emitSSet___closed__1;
-x_40 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_40, 0, x_39);
-lean_ctor_set(x_40, 1, x_38);
-return x_40;
+x_39 = l_Lean_IR_EmitC_emitSProj___closed__2;
+x_40 = lean_string_append(x_38, x_39);
+x_8 = x_40;
+goto block_33;
 }
-}
-case 1:
+case 2:
 {
 lean_object* x_41; lean_object* x_42; lean_object* x_43; 
 x_41 = lean_ctor_get(x_34, 1);
 lean_inc(x_41);
 lean_dec(x_34);
-x_42 = l_Lean_IR_EmitC_emitSProj___closed__1;
+x_42 = l_Lean_IR_EmitC_emitSProj___closed__3;
 x_43 = lean_string_append(x_41, x_42);
 x_8 = x_43;
 goto block_33;
 }
-case 2:
+case 3:
 {
 lean_object* x_44; lean_object* x_45; lean_object* x_46; 
 x_44 = lean_ctor_get(x_34, 1);
 lean_inc(x_44);
 lean_dec(x_34);
-x_45 = l_Lean_IR_EmitC_emitSProj___closed__2;
+x_45 = l_Lean_IR_EmitC_emitSProj___closed__4;
 x_46 = lean_string_append(x_44, x_45);
 x_8 = x_46;
 goto block_33;
 }
-case 3:
+case 4:
 {
 lean_object* x_47; lean_object* x_48; lean_object* x_49; 
 x_47 = lean_ctor_get(x_34, 1);
 lean_inc(x_47);
 lean_dec(x_34);
-x_48 = l_Lean_IR_EmitC_emitSProj___closed__3;
+x_48 = l_Lean_IR_EmitC_emitSProj___closed__5;
 x_49 = lean_string_append(x_47, x_48);
 x_8 = x_49;
 goto block_33;
 }
-case 4:
-{
-lean_object* x_50; lean_object* x_51; lean_object* x_52; 
-x_50 = lean_ctor_get(x_34, 1);
-lean_inc(x_50);
-lean_dec(x_34);
-x_51 = l_Lean_IR_EmitC_emitSProj___closed__4;
-x_52 = lean_string_append(x_50, x_51);
-x_8 = x_52;
-goto block_33;
-}
 default: 
 {
-uint8_t x_53; 
+uint8_t x_50; 
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
-x_53 = !lean_is_exclusive(x_34);
-if (x_53 == 0)
+x_50 = !lean_is_exclusive(x_34);
+if (x_50 == 0)
 {
-lean_object* x_54; lean_object* x_55; 
-x_54 = lean_ctor_get(x_34, 0);
-lean_dec(x_54);
-x_55 = l_Lean_IR_EmitC_emitSSet___closed__6;
+lean_object* x_51; lean_object* x_52; 
+x_51 = lean_ctor_get(x_34, 0);
+lean_dec(x_51);
+x_52 = l_Lean_IR_EmitC_emitSSet___closed__6;
 lean_ctor_set_tag(x_34, 1);
-lean_ctor_set(x_34, 0, x_55);
+lean_ctor_set(x_34, 0, x_52);
 return x_34;
 }
 else
 {
-lean_object* x_56; lean_object* x_57; lean_object* x_58; 
-x_56 = lean_ctor_get(x_34, 1);
-lean_inc(x_56);
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_34, 1);
+lean_inc(x_53);
 lean_dec(x_34);
-x_57 = l_Lean_IR_EmitC_emitSSet___closed__6;
-x_58 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_58, 0, x_57);
-lean_ctor_set(x_58, 1, x_56);
-return x_58;
+x_54 = l_Lean_IR_EmitC_emitSSet___closed__6;
+x_55 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_55, 0, x_54);
+lean_ctor_set(x_55, 1, x_53);
+return x_55;
 }
 }
 }
@@ -8226,7 +8213,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_box");
+x_1 = lean_mk_string("lean_box_float");
 return x_1;
 }
 }
@@ -8234,7 +8221,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_box_uint32");
+x_1 = lean_mk_string("lean_box");
 return x_1;
 }
 }
@@ -8242,7 +8229,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_box_uint64");
+x_1 = lean_mk_string("lean_box_uint32");
 return x_1;
 }
 }
@@ -8250,6 +8237,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__4() {
 _start:
 {
 lean_object* x_1; 
+x_1 = lean_mk_string("lean_box_uint64");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__5() {
+_start:
+{
+lean_object* x_1; 
 x_1 = lean_mk_string("lean_box_usize");
 return x_1;
 }
@@ -8260,56 +8255,58 @@ _start:
 switch (lean_obj_tag(x_1)) {
 case 0:
 {
-lean_object* x_4; lean_object* x_5; 
-x_4 = l_Lean_IR_EmitC_emitSSet___closed__1;
-x_5 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_5, 0, x_4);
-lean_ctor_set(x_5, 1, x_3);
-return x_5;
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = l_Lean_IR_EmitC_emitBoxFn___closed__1;
+x_5 = lean_string_append(x_3, x_4);
+x_6 = lean_box(0);
+x_7 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_5);
+return x_7;
 }
 case 3:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_6 = l_Lean_IR_EmitC_emitBoxFn___closed__2;
-x_7 = lean_string_append(x_3, x_6);
-x_8 = lean_box(0);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_8);
-lean_ctor_set(x_9, 1, x_7);
-return x_9;
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = l_Lean_IR_EmitC_emitBoxFn___closed__3;
+x_9 = lean_string_append(x_3, x_8);
+x_10 = lean_box(0);
+x_11 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_11, 0, x_10);
+lean_ctor_set(x_11, 1, x_9);
+return x_11;
 }
 case 4:
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_10 = l_Lean_IR_EmitC_emitBoxFn___closed__3;
-x_11 = lean_string_append(x_3, x_10);
-x_12 = lean_box(0);
-x_13 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_13, 0, x_12);
-lean_ctor_set(x_13, 1, x_11);
-return x_13;
+lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_12 = l_Lean_IR_EmitC_emitBoxFn___closed__4;
+x_13 = lean_string_append(x_3, x_12);
+x_14 = lean_box(0);
+x_15 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_15, 0, x_14);
+lean_ctor_set(x_15, 1, x_13);
+return x_15;
 }
 case 5:
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_14 = l_Lean_IR_EmitC_emitBoxFn___closed__4;
-x_15 = lean_string_append(x_3, x_14);
-x_16 = lean_box(0);
-x_17 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_17, 0, x_16);
-lean_ctor_set(x_17, 1, x_15);
-return x_17;
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_16 = l_Lean_IR_EmitC_emitBoxFn___closed__5;
+x_17 = lean_string_append(x_3, x_16);
+x_18 = lean_box(0);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_17);
+return x_19;
 }
 default: 
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_18 = l_Lean_IR_EmitC_emitBoxFn___closed__1;
-x_19 = lean_string_append(x_3, x_18);
-x_20 = lean_box(0);
-x_21 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_21, 0, x_20);
-lean_ctor_set(x_21, 1, x_19);
-return x_21;
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_20 = l_Lean_IR_EmitC_emitBoxFn___closed__2;
+x_21 = lean_string_append(x_3, x_20);
+x_22 = lean_box(0);
+x_23 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_23, 0, x_22);
+lean_ctor_set(x_23, 1, x_21);
+return x_23;
 }
 }
 }
@@ -8327,15 +8324,12 @@ return x_4;
 lean_object* l_Lean_IR_EmitC_emitBox(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; 
 x_6 = l_Lean_IR_EmitC_emitLhs(x_1, x_4, x_5);
 x_7 = lean_ctor_get(x_6, 1);
 lean_inc(x_7);
 lean_dec(x_6);
 x_8 = l_Lean_IR_EmitC_emitBoxFn(x_3, x_4, x_7);
-if (lean_obj_tag(x_8) == 0)
-{
-uint8_t x_9; 
 x_9 = !lean_is_exclusive(x_8);
 if (x_9 == 0)
 {
@@ -8385,30 +8379,6 @@ lean_ctor_set(x_35, 1, x_33);
 return x_35;
 }
 }
-else
-{
-uint8_t x_36; 
-lean_dec(x_2);
-x_36 = !lean_is_exclusive(x_8);
-if (x_36 == 0)
-{
-return x_8;
-}
-else
-{
-lean_object* x_37; lean_object* x_38; lean_object* x_39; 
-x_37 = lean_ctor_get(x_8, 0);
-x_38 = lean_ctor_get(x_8, 1);
-lean_inc(x_38);
-lean_inc(x_37);
-lean_dec(x_8);
-x_39 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_39, 0, x_37);
-lean_ctor_set(x_39, 1, x_38);
-return x_39;
-}
-}
-}
 }
 lean_object* l_Lean_IR_EmitC_emitBox___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
@@ -8424,7 +8394,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_unbox");
+x_1 = lean_mk_string("lean_unbox_float");
 return x_1;
 }
 }
@@ -8432,7 +8402,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_unbox_uint32");
+x_1 = lean_mk_string("lean_unbox");
 return x_1;
 }
 }
@@ -8440,7 +8410,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__3() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("lean_unbox_uint64");
+x_1 = lean_mk_string("lean_unbox_uint32");
 return x_1;
 }
 }
@@ -8448,6 +8418,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__4() {
 _start:
 {
 lean_object* x_1; 
+x_1 = lean_mk_string("lean_unbox_uint64");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__5() {
+_start:
+{
+lean_object* x_1; 
 x_1 = lean_mk_string("lean_unbox_usize");
 return x_1;
 }
@@ -8460,76 +8438,59 @@ x_20 = l_Lean_IR_EmitC_emitLhs(x_1, x_4, x_5);
 switch (lean_obj_tag(x_2)) {
 case 0:
 {
-uint8_t x_21; 
-lean_dec(x_3);
-x_21 = !lean_is_exclusive(x_20);
-if (x_21 == 0)
-{
-lean_object* x_22; lean_object* x_23; 
-x_22 = lean_ctor_get(x_20, 0);
-lean_dec(x_22);
-x_23 = l_Lean_IR_EmitC_emitSSet___closed__1;
-lean_ctor_set_tag(x_20, 1);
-lean_ctor_set(x_20, 0, x_23);
-return x_20;
+lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_21 = lean_ctor_get(x_20, 1);
+lean_inc(x_21);
+lean_dec(x_20);
+x_22 = l_Lean_IR_EmitC_emitUnbox___closed__1;
+x_23 = lean_string_append(x_21, x_22);
+x_6 = x_23;
+goto block_19;
 }
-else
+case 3:
 {
 lean_object* x_24; lean_object* x_25; lean_object* x_26; 
 x_24 = lean_ctor_get(x_20, 1);
 lean_inc(x_24);
 lean_dec(x_20);
-x_25 = l_Lean_IR_EmitC_emitSSet___closed__1;
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_25);
-lean_ctor_set(x_26, 1, x_24);
-return x_26;
+x_25 = l_Lean_IR_EmitC_emitUnbox___closed__3;
+x_26 = lean_string_append(x_24, x_25);
+x_6 = x_26;
+goto block_19;
 }
-}
-case 3:
+case 4:
 {
 lean_object* x_27; lean_object* x_28; lean_object* x_29; 
 x_27 = lean_ctor_get(x_20, 1);
 lean_inc(x_27);
 lean_dec(x_20);
-x_28 = l_Lean_IR_EmitC_emitUnbox___closed__2;
+x_28 = l_Lean_IR_EmitC_emitUnbox___closed__4;
 x_29 = lean_string_append(x_27, x_28);
 x_6 = x_29;
 goto block_19;
 }
-case 4:
+case 5:
 {
 lean_object* x_30; lean_object* x_31; lean_object* x_32; 
 x_30 = lean_ctor_get(x_20, 1);
 lean_inc(x_30);
 lean_dec(x_20);
-x_31 = l_Lean_IR_EmitC_emitUnbox___closed__3;
+x_31 = l_Lean_IR_EmitC_emitUnbox___closed__5;
 x_32 = lean_string_append(x_30, x_31);
 x_6 = x_32;
 goto block_19;
 }
-case 5:
+default: 
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; 
 x_33 = lean_ctor_get(x_20, 1);
 lean_inc(x_33);
 lean_dec(x_20);
-x_34 = l_Lean_IR_EmitC_emitUnbox___closed__4;
+x_34 = l_Lean_IR_EmitC_emitUnbox___closed__2;
 x_35 = lean_string_append(x_33, x_34);
 x_6 = x_35;
 goto block_19;
 }
-default: 
-{
-lean_object* x_36; lean_object* x_37; lean_object* x_38; 
-x_36 = lean_ctor_get(x_20, 1);
-lean_inc(x_36);
-lean_dec(x_20);
-x_37 = l_Lean_IR_EmitC_emitUnbox___closed__1;
-x_38 = lean_string_append(x_36, x_37);
-x_6 = x_38;
-goto block_19;
-}
 }
 block_19:
 {
@@ -13547,6 +13508,8 @@ l_Lean_IR_EmitC_emitSProj___closed__3 = _init_l_Lean_IR_EmitC_emitSProj___closed
 lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__3);
 l_Lean_IR_EmitC_emitSProj___closed__4 = _init_l_Lean_IR_EmitC_emitSProj___closed__4();
 lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__4);
+l_Lean_IR_EmitC_emitSProj___closed__5 = _init_l_Lean_IR_EmitC_emitSProj___closed__5();
+lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__5);
 l_Lean_IR_EmitC_emitExternCall___closed__1 = _init_l_Lean_IR_EmitC_emitExternCall___closed__1();
 lean_mark_persistent(l_Lean_IR_EmitC_emitExternCall___closed__1);
 l_Nat_forMAux___main___at_Lean_IR_EmitC_emitPartialApp___spec__1___closed__1 = _init_l_Nat_forMAux___main___at_Lean_IR_EmitC_emitPartialApp___spec__1___closed__1();
@@ -13573,6 +13536,8 @@ l_Lean_IR_EmitC_emitBoxFn___closed__3 = _init_l_Lean_IR_EmitC_emitBoxFn___closed
 lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__3);
 l_Lean_IR_EmitC_emitBoxFn___closed__4 = _init_l_Lean_IR_EmitC_emitBoxFn___closed__4();
 lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__4);
+l_Lean_IR_EmitC_emitBoxFn___closed__5 = _init_l_Lean_IR_EmitC_emitBoxFn___closed__5();
+lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__5);
 l_Lean_IR_EmitC_emitUnbox___closed__1 = _init_l_Lean_IR_EmitC_emitUnbox___closed__1();
 lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__1);
 l_Lean_IR_EmitC_emitUnbox___closed__2 = _init_l_Lean_IR_EmitC_emitUnbox___closed__2();
@@ -13581,6 +13546,8 @@ l_Lean_IR_EmitC_emitUnbox___closed__3 = _init_l_Lean_IR_EmitC_emitUnbox___closed
 lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__3);
 l_Lean_IR_EmitC_emitUnbox___closed__4 = _init_l_Lean_IR_EmitC_emitUnbox___closed__4();
 lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__4);
+l_Lean_IR_EmitC_emitUnbox___closed__5 = _init_l_Lean_IR_EmitC_emitUnbox___closed__5();
+lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__5);
 l_Lean_IR_EmitC_emitIsShared___closed__1 = _init_l_Lean_IR_EmitC_emitIsShared___closed__1();
 lean_mark_persistent(l_Lean_IR_EmitC_emitIsShared___closed__1);
 l_Lean_IR_EmitC_emitIsTaggedPtr___closed__1 = _init_l_Lean_IR_EmitC_emitIsTaggedPtr___closed__1();