From ba3303163d38653e718f15fd6d9e366e69ebe76b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Nov 2016 14:41:04 -0800 Subject: [PATCH] fix(library/vm/vm_nat): nat.has_decidable_eq has been renamed --- src/library/vm/vm_nat.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index 42233884e7..ee31491ebe 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -161,7 +161,7 @@ vm_obj nat_gcd(vm_obj const & a1, vm_obj const & a2) { return mk_vm_nat(r); } -vm_obj nat_has_decidable_eq(vm_obj const & a1, vm_obj const & a2) { +vm_obj nat_decidable_eq(vm_obj const & a1, vm_obj const & a2) { if (is_simple(a1) && is_simple(a2)) { return mk_vm_bool(cidx(a1) == cidx(a2)); } else { @@ -233,7 +233,7 @@ void initialize_vm_nat() { DECLARE_VM_BUILTIN(name({"nat", "div"}), nat_div); DECLARE_VM_BUILTIN(name({"nat", "mod"}), nat_mod); DECLARE_VM_BUILTIN(name({"nat", "gcd"}), nat_gcd); - DECLARE_VM_BUILTIN(name({"nat", "has_decidable_eq"}), nat_has_decidable_eq); + DECLARE_VM_BUILTIN(name({"nat", "decidable_eq"}), nat_decidable_eq); DECLARE_VM_BUILTIN(name({"nat", "decidable_le"}), nat_decidable_le); DECLARE_VM_BUILTIN(name({"nat", "decidable_lt"}), nat_decidable_lt); DECLARE_VM_BUILTIN(name({"nat", "to_string"}), nat_to_string);