Update for review

clementblaudeau · clementblaudeau · commit 88782a070396 · 2025-06-10T11:57:13.000+02:00
diff --git a/hax-lib/proof-libs/fstar/core/Core.Fmt.fsti b/hax-lib/proof-libs/fstar/core/Core.Fmt.fsti
@@ -63,5 +63,6 @@ instance debuggable_pair (#a:Type) (#b:Type) (x: t_Debug a) (y: t_Debug b): t_De
      | Core.Result.Result_Err e -> (fmt_a, result_a));
 }
 
+/// Default empty implementation, used for lax-checking
 [@FStar.Tactics.Typeclasses.tcinstance]
 val derive_debug (#t: Type) : t_Debug t
diff --git a/hax-lib/proof-libs/fstar/core/Core.Str.Iter.fsti b/hax-lib/proof-libs/fstar/core/Core.Str.Iter.fsti
@@ -7,4 +7,4 @@ type t_Split (pattern: Type)
 /// Basic implementations
 
 [@FStar.Tactics.Typeclasses.tcinstance]
-val impl_t_split_any (#t:Type): (t_Split Rust_primitives.Char.char)
+val impl_t_split_char: (t_Split Rust_primitives.Char.char)

Original file line number	Diff line number	Diff line change
`@@ -63,5 +63,6 @@ instance debuggable_pair (#a:Type) (#b:Type) (x: t_Debug a) (y: t_Debug b): t_De`
`63`	`63`	`\| Core.Result.Result_Err e -> (fmt_a, result_a));`
`64`	`64`	`}`
`65`	`65`
	`66`	`+/// Default empty implementation, used for lax-checking`
`66`	`67`	`[@FStar.Tactics.Typeclasses.tcinstance]`
`67`	`68`	`val derive_debug (#t: Type) : t_Debug t`