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
|
Toplevel input, character 0:
> From Coq Require Import ssreflect ssrfun.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
Datatypes_prod__canonical__compress_coe_D =
fun D D' : D.type =>
{|
D.sort := D.sort D * D.sort D';
D.class :=
{|
D.compress_coe_hasA_mixin :=
prodA (compress_coe_D__to__compress_coe_A D)
(compress_coe_D__to__compress_coe_A D');
D.compress_coe_hasB_mixin :=
prodB tt (compress_coe_D__to__compress_coe_B D)
(compress_coe_D__to__compress_coe_B D');
D.compress_coe_hasC_mixin :=
prodC tt tt (compress_coe_D__to__compress_coe_C D)
(compress_coe_D__to__compress_coe_C D');
D.compress_coe_hasD_mixin := prodD D D'
|}
|}
: D.type -> D.type -> D.type
Arguments Datatypes_prod__canonical__compress_coe_D D D'
|
