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

fix: bug at ir.cpp

Browse source
This commit is contained in:
Leonardo de Moura 2020-04-03 17:39:28 -07:00
parent a84c177cb5
commit 485034bbba
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Data/Float.lean
View file

@ -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

2
src/library/compiler/ir.cpp
View file

@ -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 {