More examples

dk_obj_examples.dk

-#NAME dk_obj_examples
+#NAME dk_obj_examples.
 
 Label := dk_obj.Label.
 type := dk_obj.ObjType.
@@ -363,3 +363,72 @@ test8 := dk_obj.select
           l_get.
 
 test9 := dk_obj.select promCell myCell l_contents.
+
+
+
+(; Classes ;)
+l_new : Label
+:=
+  dk_string.cons dk_char.n (
+  dk_string.cons dk_char.e (
+  dk_string.cons dk_char.w (
+  dk_string.nil))).
+
+filtermaptype : (Label -> dk_bool.Bool) ->
+                (type -> type) ->
+                type ->
+                type.
+[] filtermaptype _ _ dk_type.nil --> dk_type.nil
+[ P : Label -> dk_bool.Bool,
+  f : type -> type,
+  l : Label,
+  A : type,
+  B : type ]
+    filtermaptype P f (dk_type.cons l A B)
+      -->
+    dk_type.if
+      (P l)
+      (dk_type.cons l (f A) B)
+      B.
+
+trait : type -> dk_domain.Domain -> type.
+[ A : type,
+  D : dk_domain.Domain ]
+    trait A D
+      -->
+    filtermaptype
+      (l : Label => dk_domain.mem l D)
+      (arrow A)
+      A.
+
+type_sub : type -> dk_domain.Domain -> type.
+[ A : type,
+  D : dk_domain.Domain ]
+    type_sub A D
+      -->
+    filtermaptype
+      (l : Label => dk_domain.mem l D)
+      (B : type => B)
+      A.
+
+ins_sub_Class : type ->
+                dk_domain.Domain ->
+                dk_domain.Domain ->
+                type.
+[ A : type,
+  Ins : dk_domain.Domain,
+  Sub : dk_domain.Domain ]
+    ins_sub_Class A Ins Sub
+      -->
+    dk_type.cons
+      l_new
+      (type_sub A Ins)
+      (trait A Sub).
+
+Class : type -> type.
+[ A : type ]
+    Class A
+      -->
+    ins_sub_Class A (dk_type.domain A) (dk_type.domain A).
+
+(; ins_sub_class :  ;)