1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
From HB Require Import structures.
#[key="A"]
HB.mixin Record m1 (T : Type) (A : Type) := {
inhab : A;
inhab_param : T;
}.
HB.structure Definition s1 T := { A of m1 T A }.
Check inhab.
(* inhab : forall (T : Type) (A : s1.type T), s1.sort A *)
HB.instance Definition nat_m1 := m1.Build bool nat 7 false.
Check (refl_equal _ : @inhab _ _ = 7).
HB.instance Definition list_m1 A := m1.Build (option A) (list nat) (cons 7 nil) None.
Check (refl_equal _ : @inhab _ _ = (cons 7 nil)).
HB.mixin Record m2 (T : Type) (A : Type) of m1 T A := {
inj : T -> A;
}.
HB.structure Definition s2 T :=
{ A of m1 T A & m2 T A }.
Check fun X : s2.type nat => inhab : X.
Check fun X : s2.type nat => inj : nat -> X.
About s2_to_s1.
|
