diff --git a/src/library/parray.h b/src/library/parray.h index a792abfe9b..9f6ca0fec0 100644 --- a/src/library/parray.h +++ b/src/library/parray.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include #include #include "util/memory_pool.h" diff --git a/src/library/vm/vm_array.cpp b/src/library/vm/vm_array.cpp index 46ed5b397d..1bdc2b6ab7 100644 --- a/src/library/vm/vm_array.cpp +++ b/src/library/vm/vm_array.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "library/parray.h" #include "library/vm/vm.h" #include "library/vm/vm_nat.h" diff --git a/src/tests/library/parray.cpp b/src/tests/library/parray.cpp index bc2cbc8da7..15b30aa388 100644 --- a/src/tests/library/parray.cpp +++ b/src/tests/library/parray.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include #include #include "util/test.h" diff --git a/tests/lean/run/smt_array.lean b/tests/lean/run/smt_array.lean index bcc80cb52e..03aca38f6a 100644 --- a/tests/lean/run/smt_array.lean +++ b/tests/lean/run/smt_array.lean @@ -1,3 +1,4 @@ +namespace hide constant array : Type constant read : array → nat → nat constant write : array → nat → nat → array @@ -16,3 +17,5 @@ read a5 4 = read a1 4 begin [smt] intros, eblast end + +end hide