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/lean/Traits | |
| parent | 1c8187d7f4129e09f23d3b5caf33938a0c91ea77 (diff) | |
Regenerate the files
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Traits.lean | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 9ac4736c..e7795d9c 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -326,15 +326,11 @@ def test_where2 := Result.ret () -/- [alloc::string::String] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 -/ -axiom alloc.string.String : Type - /- Trait declaration: [traits::ParentTrait0] Source: 'src/traits.rs', lines 200:0-200:22 -/ structure ParentTrait0 (Self : Type) where W : Type - get_name : Self → Result alloc.string.String + get_name : Self → Result String get_w : Self → Result W /- Trait declaration: [traits::ParentTrait1] @@ -350,9 +346,7 @@ structure ChildTrait (Self : Type) where /- [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 -/ def test_child_trait1 - (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : - Result alloc.string.String - := + (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String := ChildTraitTInst.ParentTrait0SelfInst.get_name x /- [traits::test_child_trait2]: forward function |