Skip to content

Commit

Permalink
Cleanup sandwich core changes.
Browse files Browse the repository at this point in the history
  • Loading branch information
maximebuyse committed Dec 17, 2024
1 parent b361b33 commit 055233d
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 5 deletions.
4 changes: 0 additions & 4 deletions proof-libs/fstar/core/Alloc.Vec.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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



2 changes: 1 addition & 1 deletion proof-libs/fstar/core/Core.Ptr.Non_null.fsti
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
module Core.Ptr.Non_null

val t_NonNull (v_T: Type0) : eqtype
val t_NonNull (v_T: Type0) : eqtype

0 comments on commit 055233d

Please sign in to comment.