diff options
author | Son Ho | 2023-11-07 10:44:58 +0100 |
---|---|---|
committer | Son Ho | 2023-11-07 10:44:58 +0100 |
commit | a745e81c9949f24878f788fffd36667739c59330 (patch) | |
tree | 92ef105feb065deff71c72204ea18b3624b377e0 /tests | |
parent | ed788eec1d8be1656c0ad7dab25975ad3f5497c2 (diff) |
Update the extraction
Diffstat (limited to 'tests')
-rw-r--r-- | tests/lean/Traits/Funs.lean | 9 | ||||
-rw-r--r-- | tests/lean/Traits/Types.lean | 4 |
2 files changed, 13 insertions, 0 deletions
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean index 156ef1e0..6a2834ff 100644 --- a/tests/lean/Traits/Funs.lean +++ b/tests/lean/Traits/Funs.lean @@ -227,6 +227,15 @@ def order1 := Result.ret () +/- Trait implementation: [traits::usize::{9}] -/ +def usize.ParentTrait1Inst : ParentTrait1 Usize := { +} + +/- Trait implementation: [traits::usize::{10}] -/ +def usize.ChildTrait1Inst : ChildTrait1 Usize := { + parent_clause_0 := usize.ParentTrait1Inst +} + /- [traits::map_option]: forward function -/ def map_option (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) : diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean index e325da6f..20af9cb1 100644 --- a/tests/lean/Traits/Types.lean +++ b/tests/lean/Traits/Types.lean @@ -72,6 +72,10 @@ structure ChildTrait (Self : Type) where parent_clause_0 : ParentTrait0 Self parent_clause_1 : ParentTrait1 Self +/- Trait declaration: [traits::ChildTrait1] -/ +structure ChildTrait1 (Self : Type) where + parent_clause_0 : ParentTrait1 Self + /- Trait declaration: [traits::Iterator] -/ structure Iterator (Self : Type) where Item : Type |