summaryrefslogtreecommitdiff
path: root/tests/fstar/traits
diff options
context:
space:
mode:
authorSon Ho2023-11-24 17:41:42 +0100
committerSon Ho2023-11-24 17:41:42 +0100
commitd84040e000333d6d2a212fb849a38fb73a65eb48 (patch)
treec15309842c8e37b533171e1f6e44a5362cbde292 /tests/fstar/traits
parent1c8187d7f4129e09f23d3b5caf33938a0c91ea77 (diff)
Regenerate the files
Diffstat (limited to 'tests/fstar/traits')
-rw-r--r--tests/fstar/traits/Traits.fst10
1 files changed, 2 insertions, 8 deletions
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 4cb9fbf1..895a1cac 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -307,15 +307,11 @@ let test_where2
=
Return ()
-(** [alloc::string::String]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *)
-assume type alloc_string_String_t : Type0
-
(** Trait declaration: [traits::ParentTrait0]
Source: 'src/traits.rs', lines 200:0-200:22 *)
noeq type parentTrait0_t (self : Type0) = {
tW : Type0;
- get_name : self -> result alloc_string_String_t;
+ get_name : self -> result string;
get_w : self -> result tW;
}
@@ -333,9 +329,7 @@ noeq type childTrait_t (self : Type0) = {
(** [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 *)
let test_child_trait1
- (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
- result alloc_string_String_t
- =
+ (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
childTraitTInst.parentTrait0SelfInst.get_name x
(** [traits::test_child_trait2]: forward function