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.
HB.mixin Record InhMixin T := {
point : T;
}.
HB.structure Definition Inh := { T of InhMixin T }.
HB.instance Definition nat_inh := InhMixin.Build nat 0.
Section ProdInh.
Variables (T S : Inh.type).
(* This works fine *)
HB.instance Definition prod_inh :=
InhMixin.Build (T * S)%type (point, point).
End ProdInh.
Section FunInh.
Variables (T S : Inh.type).
HB.instance Definition fun_inh :=
InhMixin.Build (T -> S) (fun _ => point).
End FunInh.
|
