From 995a54b1f80bbb19e2a0a925cadf8b300f911bdf Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 30 Apr 2024 16:54:50 +0200 Subject: [PATCH] add neon types to F* core model --- proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti diff --git a/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti b/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti new file mode 100644 index 000000000..5772fa15c --- /dev/null +++ b/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti @@ -0,0 +1,8 @@ +module Core.Core_arch.Arm_shared.Neon + +val t_int16x4_t:Type0 +val t_int32x2_t:Type0 +val t_int32x4_t:Type0 +val t_int64x2_t:Type0 +val t_uint32x4_t:Type0 +val t_uint8x16_t:Type0