Merge pull request #1292 from cryspen/fstar-core-additions-and-fixes

Additions and corrections in F* core lib.

proof-libs/fstar/core/Alloc.Collections.Btree.Set.fsti

@@ -10,3 +10,17 @@ val impl_13__new #t (): t_BTreeSet t ()
 val impl_14__len #t #u (x:t_BTreeSet t u) : usize
 
 val impl_14__insert #t #u (x:t_BTreeSet t u) (y:t) : (t_BTreeSet t u & bool)
+
+val btree_iter_iter (t: Type0): Core.Iter.Traits.Iterator.iterator (t_Iter t)
+
+val impl_14__iter #t #u (x:t_BTreeSet t u): t_Iter t
+
+unfold instance impl t : Core.Iter.Traits.Iterator.iterator (t_Iter t) = {
+  f_Item = t;
+  f_next = (btree_iter_iter t).f_next;
+  f_contains = (btree_iter_iter t).f_contains;
+  f_fold = (btree_iter_iter t).f_fold;
+  f_enumerate = (btree_iter_iter t).f_enumerate;
+  f_step_by = (btree_iter_iter t).f_step_by;
+  f_all = (btree_iter_iter t).f_all;
+}

proof-libs/fstar/core/Core.Cmp.fsti

@@ -28,15 +28,15 @@ type t_Ordering =
 
 
 class t_PartialOrd (v_Self: Type) (v_Rhs:Type) = {
-  _super_9014672428308350468: t_PartialEq v_Self v_Rhs;
+  _super_8303539986193044559: t_PartialEq v_Self v_Rhs;
   f_partial_cmp_pre: v_Self -> v_Rhs -> Type0;
   f_partial_cmp_post: v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering -> Type0;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
 }
 
 class t_Ord (v_Self: Type) = {
-  _super_8099741844003281729: t_Eq v_Self;
-  _super_12866954522599331834: t_PartialOrd v_Self v_Self;
+  _super_8438227699474489191: t_Eq v_Self;
+  _super_17497397511932837737: t_PartialOrd v_Self v_Self;
   f_cmp_pre: v_Self -> v_Self -> Type0;
   f_cmp_post: v_Self -> v_Self -> t_Ordering -> Type0;
   f_cmp:v_Self -> v_Self -> t_Ordering;

proof-libs/fstar/core/Core.Convert.fst

@@ -17,14 +17,22 @@ instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len)
   )
 }
 
-
 instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core.Slice.impl__len s == len}) (t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t {Core.Slice.impl__len s == len}) -> 
     Core.Result.Result_Ok (s <: t_Array t len)
   )
 }
 
+instance integer_try_into (t:inttype) (t':inttype) : try_into_tc (int_t t) (int_t t') = {
+  f_Error = Core.Num.Error.t_TryFromIntError;
+  f_try_into = (fun (x: int_t t) ->
+    if range (v #t x) t'
+    then Core.Result.Result_Ok (Rust_primitives.Integers.cast #t #t' x)
+    else Core.Result.Result_Err ()
+  )
+}
+
 class t_Into self t = {
   f_into_pre: self -> bool;
   f_into_post: self -> t -> bool;