Skip to content

Commit 164d561

Browse files
proux01proux01
committed
Fix test-suite
1 parent 717ef2b commit 164d561

16 files changed

+659
-3
lines changed

‎tests/about.v.out‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1+
Toplevel input, character 0:
2+
> From Coq Require Import ZArith ssrfun ssreflect.
3+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
Warning: "From Coq" has been replaced by "From Stdlib".
5+
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
16
HB: AddMonoid_of_TYPE is a factory
27
(from "./examples/demo1/hierarchy_5.v", line 10)
38
HB: AddMonoid_of_TYPE operations and axioms are:

‎tests/about.v.out.18‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
HB: AddMonoid_of_TYPE is a factory
2+
(from "./examples/demo1/hierarchy_5.v", line 10)
3+
HB: AddMonoid_of_TYPE operations and axioms are:
4+
- zero
5+
- add
6+
- addrA
7+
- add0r
8+
- addr0
9+
HB: AddMonoid_of_TYPE requires the following mixins:
10+
HB: AddMonoid_of_TYPE provides the following mixins:
11+
- AddMonoid_of_TYPE
12+
HB: AddMonoid_of_TYPE.Build is a factory constructor
13+
(from "./examples/demo1/hierarchy_5.v", line 10)
14+
HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
15+
HB: AddMonoid_of_TYPE.Build provides the following mixins:
16+
- AddMonoid_of_TYPE
17+
HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
18+
- S : Type
19+
- zero : AddMonoid.sort S
20+
- add : S -> S -> S
21+
- addrA : associative add
22+
- add0r : left_id 0%G add
23+
- addr0 : right_id 0%G add
24+
HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
25+
HB: AddAG.type characterizing operations and axioms are:
26+
- addNr
27+
- opp
28+
HB: AddAG is a factory for the following mixins:
29+
- AddMonoid_of_TYPE
30+
- AddComoid_of_AddMonoid
31+
- AddAG_of_AddComoid (* new, not from inheritance *)
32+
HB: AddAG inherits from:
33+
- AddMonoid
34+
- AddComoid
35+
HB: AddAG is inherited by:
36+
- Ring
37+
HB: AddMonoid.type is a structure
38+
(from "./examples/demo1/hierarchy_5.v", line 17)
39+
HB: AddMonoid.type characterizing operations and axioms are:
40+
- addr0
41+
- add0r
42+
- addrA
43+
- add
44+
- zero
45+
HB: AddMonoid is a factory for the following mixins:
46+
- AddMonoid_of_TYPE (* new, not from inheritance *)
47+
HB: AddMonoid inherits from:
48+
HB: AddMonoid is inherited by:
49+
- AddComoid
50+
- AddAG
51+
- BiNearRing
52+
- SemiRing
53+
- Ring
54+
HB: Ring_of_AddAG is a factory
55+
(from "./examples/demo1/hierarchy_5.v", line 108)
56+
HB: Ring_of_AddAG operations and axioms are:
57+
- one
58+
- mul
59+
- mulrA
60+
- mulr1
61+
- mul1r
62+
- mulrDl
63+
- mulrDr
64+
HB: Ring_of_AddAG requires the following mixins:
65+
- AddMonoid_of_TYPE
66+
- AddComoid_of_AddMonoid
67+
- AddAG_of_AddComoid
68+
HB: Ring_of_AddAG provides the following mixins:
69+
- BiNearRing_of_AddMonoid
70+
Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
71+
mul0r are derived from addrC and the other ring axioms, following a proof
72+
of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
73+
theory. In Near-rings and near-fields. Proceedings of the conference held
74+
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
75+
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
76+
1995).
77+
HB: Ring_of_AddAG.Build is a factory constructor
78+
(from "./examples/demo1/hierarchy_5.v", line 108)
79+
HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
80+
- AddMonoid_of_TYPE
81+
- AddComoid_of_AddMonoid
82+
- AddAG_of_AddComoid
83+
HB: Ring_of_AddAG.Build provides the following mixins:
84+
- BiNearRing_of_AddMonoid
85+
HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr
86+
- A : Type
87+
- one : A
88+
- mul : A -> A -> A
89+
- mulrA : associative mul
90+
- mulr1 : left_id one mul
91+
- mul1r : right_id one mul
92+
- mulrDl : left_distributive mul add
93+
- mulrDr : right_distributive mul add
94+
Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
95+
mul0r are derived from addrC and the other ring axioms, following a proof
96+
of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
97+
theory. In Near-rings and near-fields. Proceedings of the conference held
98+
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
99+
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
100+
1995).
101+
HB: add is an operation of structure AddMonoid
102+
(from "./examples/demo1/hierarchy_5.v", line 17)
103+
HB: add comes from mixin AddMonoid_of_TYPE
104+
(from "./examples/demo1/hierarchy_5.v", line 10)
105+
HB: AddAG.sort is a canonical projection
106+
(from "./examples/demo1/hierarchy_5.v", line 73)
107+
HB: AddAG.sort has the following canonical values:
108+
- Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
109+
- Z
110+
HB: AddAG.sort is a coercion from AddAG to Sortclass
111+
(from "./examples/demo1/hierarchy_5.v", line 73)
112+
HB: Z is canonically equipped with structures:
113+
- AddMonoid
114+
AddComoid
115+
AddAG
116+
(from "(stdin)", line 5)
117+
- BiNearRing
118+
SemiRing
119+
Ring
120+
(from "(stdin)", line 10)
121+
HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
122+
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
123+
HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
124+
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
125+
Toplevel input, character 15:
126+
> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid.
127+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
128+
Error:
129+
HB: unable to locate
130+
Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid
131+
HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
132+
Interactive Module hierarchy_5 started
133+
Interactive Module AddComoid started
134+
HB: Z is canonically equipped with structures:
135+
- AddMonoid
136+
demo1.hierarchy_5.AddComoid
137+
AddAG
138+
(from "(stdin)", line 5)
139+
- BiNearRing
140+
SemiRing
141+
Ring
142+
(from "(stdin)", line 10)

‎tests/about.v.out.19‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
HB: AddMonoid_of_TYPE is a factory
2+
(from "./examples/demo1/hierarchy_5.v", line 10)
3+
HB: AddMonoid_of_TYPE operations and axioms are:
4+
- zero
5+
- add
6+
- addrA
7+
- add0r
8+
- addr0
9+
HB: AddMonoid_of_TYPE requires the following mixins:
10+
HB: AddMonoid_of_TYPE provides the following mixins:
11+
- AddMonoid_of_TYPE
12+
HB: AddMonoid_of_TYPE.Build is a factory constructor
13+
(from "./examples/demo1/hierarchy_5.v", line 10)
14+
HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with:
15+
HB: AddMonoid_of_TYPE.Build provides the following mixins:
16+
- AddMonoid_of_TYPE
17+
HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0
18+
- S : Type
19+
- zero : AddMonoid.sort S
20+
- add : S -> S -> S
21+
- addrA : associative add
22+
- add0r : left_id 0%G add
23+
- addr0 : right_id 0%G add
24+
HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73)
25+
HB: AddAG.type characterizing operations and axioms are:
26+
- addNr
27+
- opp
28+
HB: AddAG is a factory for the following mixins:
29+
- AddMonoid_of_TYPE
30+
- AddComoid_of_AddMonoid
31+
- AddAG_of_AddComoid (* new, not from inheritance *)
32+
HB: AddAG inherits from:
33+
- AddMonoid
34+
- AddComoid
35+
HB: AddAG is inherited by:
36+
- Ring
37+
HB: AddMonoid.type is a structure
38+
(from "./examples/demo1/hierarchy_5.v", line 17)
39+
HB: AddMonoid.type characterizing operations and axioms are:
40+
- addr0
41+
- add0r
42+
- addrA
43+
- add
44+
- zero
45+
HB: AddMonoid is a factory for the following mixins:
46+
- AddMonoid_of_TYPE (* new, not from inheritance *)
47+
HB: AddMonoid inherits from:
48+
HB: AddMonoid is inherited by:
49+
- AddComoid
50+
- AddAG
51+
- BiNearRing
52+
- SemiRing
53+
- Ring
54+
HB: Ring_of_AddAG is a factory
55+
(from "./examples/demo1/hierarchy_5.v", line 108)
56+
HB: Ring_of_AddAG operations and axioms are:
57+
- one
58+
- mul
59+
- mulrA
60+
- mulr1
61+
- mul1r
62+
- mulrDl
63+
- mulrDr
64+
HB: Ring_of_AddAG requires the following mixins:
65+
- AddMonoid_of_TYPE
66+
- AddComoid_of_AddMonoid
67+
- AddAG_of_AddComoid
68+
HB: Ring_of_AddAG provides the following mixins:
69+
- BiNearRing_of_AddMonoid
70+
Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
71+
mul0r are derived from addrC and the other ring axioms, following a proof
72+
of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
73+
theory. In Near-rings and near-fields. Proceedings of the conference held
74+
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
75+
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
76+
1995).
77+
HB: Ring_of_AddAG.Build is a factory constructor
78+
(from "./examples/demo1/hierarchy_5.v", line 108)
79+
HB: Ring_of_AddAG.Build requires its subject to be already equipped with:
80+
- AddMonoid_of_TYPE
81+
- AddComoid_of_AddMonoid
82+
- AddAG_of_AddComoid
83+
HB: Ring_of_AddAG.Build provides the following mixins:
84+
- BiNearRing_of_AddMonoid
85+
HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr
86+
- A : Type
87+
- one : A
88+
- mul : A -> A -> A
89+
- mulrA : associative mul
90+
- mulr1 : left_id one mul
91+
- mul1r : right_id one mul
92+
- mulrDl : left_distributive mul add
93+
- mulrDr : right_distributive mul add
94+
Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and
95+
mul0r are derived from addrC and the other ring axioms, following a proof
96+
of Hankel (Gerhard Betsch. On the beginnings and development of near-ring
97+
theory. In Near-rings and near-fields. Proceedings of the conference held
98+
in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics
99+
and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht,
100+
1995).
101+
HB: add is an operation of structure AddMonoid
102+
(from "./examples/demo1/hierarchy_5.v", line 17)
103+
HB: add comes from mixin AddMonoid_of_TYPE
104+
(from "./examples/demo1/hierarchy_5.v", line 10)
105+
HB: AddAG.sort is a canonical projection
106+
(from "./examples/demo1/hierarchy_5.v", line 73)
107+
HB: AddAG.sort has the following canonical values:
108+
- Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196)
109+
- Z
110+
HB: AddAG.sort is a coercion from AddAG to Sortclass
111+
(from "./examples/demo1/hierarchy_5.v", line 73)
112+
HB: Z is canonically equipped with structures:
113+
- AddMonoid
114+
AddComoid
115+
AddAG
116+
(from "(stdin)", line 5)
117+
- BiNearRing
118+
SemiRing
119+
Ring
120+
(from "(stdin)", line 10)
121+
HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from
122+
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
123+
HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from
124+
Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196)
125+
Toplevel input, character 15:
126+
> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid.
127+
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
128+
Error:
129+
HB: unable to locate
130+
Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid
131+
HB: synthesized in file File "(stdin)", line 5, column 0, character 127:
132+
Interactive Module hierarchy_5 started
133+
Interactive Module AddComoid started
134+
HB: Z is canonically equipped with structures:
135+
- AddMonoid
136+
demo1.hierarchy_5.AddComoid
137+
AddAG
138+
(from "(stdin)", line 5)
139+
- BiNearRing
140+
SemiRing
141+
Ring
142+
(from "(stdin)", line 10)

0 commit comments

Comments
 (0)