diff options
author | Son Ho | 2023-11-24 17:41:42 +0100 |
---|---|---|
committer | Son Ho | 2023-11-24 17:41:42 +0100 |
commit | d84040e000333d6d2a212fb849a38fb73a65eb48 (patch) | |
tree | c15309842c8e37b533171e1f6e44a5362cbde292 /tests/fstar/traits | |
parent | 1c8187d7f4129e09f23d3b5caf33938a0c91ea77 (diff) |
Regenerate the files
Diffstat (limited to 'tests/fstar/traits')
-rw-r--r-- | tests/fstar/traits/Traits.fst | 10 |
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 |