Merge pull request #1353 from cryspen/fix-try-into

fix(proof-libs/F*): fix name `f_TryInto`

Author: W95Psp

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

@@ -2,13 +2,13 @@
 module Core.Convert
 open Rust_primitives
 
-class try_into_tc self t = {
+class t_TryInto self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
   f_try_into: self -> Core.Result.t_Result t f_Error
 }
 
-instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len) = {
+instance impl_6 (t: Type0) (len: usize): t_TryInto (t_Slice t) (t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t) -> 
     if Core.Slice.impl__len s = len
@@ -17,14 +17,14 @@ 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) = {
+instance impl_6_refined (t: Type0) (len: usize): t_TryInto (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') = {
+instance integer_try_into (t:inttype) (t':inttype) : t_TryInto (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'