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

fix(library/compiler/builtin): incorrect builtin type

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-29 16:04:02 -08:00
parent bb43567273
commit 706f4cb01b
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/compiler/builtin.cpp
View file

@ -89,6 +89,7 @@ void initialize_builtin() {
expr o_o_o = mk_arrow(o, o_o);
expr o_o_o_o = mk_arrow(o, o_o_o);
expr o_u32_o = mk_arrow(o, mk_arrow(u32, o));
expr o_u32 = mk_arrow(o, u32);
expr o_u8 = mk_arrow(o, u8);
expr o_u8_u8_o_o = mk_arrow(o, mk_arrow(u8, mk_arrow(u8, o_o)));
list<bool> b{true};
@ -133,7 +134,7 @@ void initialize_builtin() {
register_builtin(name({"string", "mk_iterator"}), o_o, "string_mk_iterator", c);
register_builtin(name({"string", "dec_eq"}), o_o_o, "string_dec_eq", bb);
register_builtin(name({"string", "dec_lt"}), o_o_o, "string_dec_lt", bb);
register_builtin(name({"string", "iterator", "curr"}), o_o, "string_iterator_curr", b);
register_builtin(name({"string", "iterator", "curr"}), o_u32, "string_iterator_curr", b);
register_builtin(name({"string", "iterator", "set_curr"}), o_u32_o, "string_iterator_set_curr", cc);
register_builtin(name({"string", "iterator", "next"}), o_o, "string_iterator_next", c);
register_builtin(name({"string", "iterator", "prev"}), o_o, "string_iterator_prev", c);