From 485034bbbaeccec802c2dc117b0d1c5846e6d99d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Apr 2020 17:39:28 -0700
Subject: [PATCH] fix: bug at ir.cpp

---
 src/Init/Data/Float.lean    | 7 +++++++
 src/library/compiler/ir.cpp | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 97e0dede14..401c347c39 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -68,6 +68,13 @@ match a, b with
 match a, b with
 | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
+instance floatDecEq : DecidableEq Float := Float.decEq
+instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
+instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
+
 @[extern "lean_float_to_string"] constant Float.toString : Float → String := arbitrary _
 
 instance : HasToString Float := ⟨Float.toString⟩
+
+abbrev Nat.toFloat (n : Nat) : Float :=
+Float.ofNat n
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index 73c154e80c..e0ae30fc9b 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -445,7 +445,7 @@ class to_ir_fn {
                 expr new_fvar   = m_lctx.mk_local_decl(ngen(), n, type, val);
                 fvars.push_back(new_fvar);
                 expr const & op = get_app_fn(val);
-                if (is_llnf_sset(op) || is_llnf_uset(op)) {
+                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_uset(op)) {
                     /* In the Lean IR, sset and uset are instructions that perform destructive updates. */
                     subst.push_back(app_arg(app_fn(val)));
                 } else {