From 055233d939216061fcde88fa7631665ed21fc0f9 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 17 Dec 2024 15:35:11 +0100 Subject: [PATCH] Cleanup sandwich core changes. --- proof-libs/fstar/core/Alloc.Vec.fst | 4 ---- proof-libs/fstar/core/Core.Ptr.Non_null.fsti | 2 +- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst index 42aa58a32..6e3b411e1 100644 --- a/proof-libs/fstar/core/Alloc.Vec.fst +++ b/proof-libs/fstar/core/Alloc.Vec.fst @@ -3,7 +3,6 @@ open Rust_primitives unfold type t_Vec t (_: unit) = s:t_Slice t - let impl__new #t (): t_Vec t () = FStar.Seq.empty let impl_2__extend_from_slice #t (#[(Tactics.exact (`()))]alloc:unit) (self: t_Vec t alloc) (other: t_Slice t{Seq.length self + Seq.length other <= max_usize}): t_Vec t alloc @@ -39,6 +38,3 @@ instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = { let impl_1__is_empty #t (#[(Tactics.exact (`()))]alloc:unit) (v: t_Vec t alloc): bool = Seq.length v = 0 - - - diff --git a/proof-libs/fstar/core/Core.Ptr.Non_null.fsti b/proof-libs/fstar/core/Core.Ptr.Non_null.fsti index 144534ea4..935931900 100644 --- a/proof-libs/fstar/core/Core.Ptr.Non_null.fsti +++ b/proof-libs/fstar/core/Core.Ptr.Non_null.fsti @@ -1,3 +1,3 @@ module Core.Ptr.Non_null -val t_NonNull (v_T: Type0) : eqtype \ No newline at end of file +val t_NonNull (v_T: Type0) : eqtype