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

fix(library/vm/vm_string): we were not using the builtin implementation for string.decidable_eq

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-14 09:48:43 -08:00
parent 600b7ceb28
commit 49d779e3a6
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/vm/vm_string.cpp
View file

@ -502,8 +502,8 @@ void initialize_vm_string() {
DECLARE_VM_BUILTIN(name({"string", "to_list"}), string_to_list);
DECLARE_VM_BUILTIN(name({"string", "fold"}), string_fold);
DECLARE_VM_BUILTIN(name({"string", "mk_iterator"}), string_mk_iterator);
DECLARE_VM_BUILTIN(name({"string", "has_decidable_eq"}), string_has_decidable_eq);
// DECLARE_VM_BUILTIN(name({"string", "cmp"}), string_cmp);
DECLARE_VM_BUILTIN(name({"string", "decidable_eq"}), string_has_decidable_eq);
// DECLARE_VM_BUILTIN(name({"string", "cmp"}), string_cmp);
DECLARE_VM_BUILTIN(name({"string", "has_decidable_lt"}), string_has_decidable_lt);
DECLARE_VM_BUILTIN(name({"string", "hash"}), string_hash);