summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/lean/Traits/Funs.lean9
-rw-r--r--tests/lean/Traits/Types.lean4
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