diff --git a/tests/about.v.out b/tests/about.v.out index 3ac71cc29..726956a80 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -1,3 +1,8 @@ +Toplevel input, character 0: +> From Coq Require Import ZArith ssrfun ssreflect. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning: "From Coq" has been replaced by "From Stdlib". +[deprecated-from-Coq,deprecated-since-9.0,deprecated,default] HB: AddMonoid_of_TYPE is a factory (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddMonoid_of_TYPE operations and axioms are: diff --git a/tests/about.v.out.18 b/tests/about.v.out.18 new file mode 100644 index 000000000..3ac71cc29 --- /dev/null +++ b/tests/about.v.out.18 @@ -0,0 +1,142 @@ +HB: AddMonoid_of_TYPE is a factory + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE operations and axioms are: + - zero + - add + - addrA + - add0r + - addr0 +HB: AddMonoid_of_TYPE requires the following mixins: +HB: AddMonoid_of_TYPE provides the following mixins: + - AddMonoid_of_TYPE +HB: AddMonoid_of_TYPE.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: +HB: AddMonoid_of_TYPE.Build provides the following mixins: + - AddMonoid_of_TYPE +HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 + - S : Type + - zero : AddMonoid.sort S + - add : S -> S -> S + - addrA : associative add + - add0r : left_id 0%G add + - addr0 : right_id 0%G add +HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.type characterizing operations and axioms are: + - addNr + - opp +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring +HB: AddMonoid.type is a structure + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: AddMonoid.type characterizing operations and axioms are: + - addr0 + - add0r + - addrA + - add + - zero +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring +HB: Ring_of_AddAG is a factory + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG operations and axioms are: + - one + - mul + - mulrA + - mulr1 + - mul1r + - mulrDl + - mulrDr +HB: Ring_of_AddAG requires the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG provides the following mixins: + - BiNearRing_of_AddMonoid +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: Ring_of_AddAG.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG.Build requires its subject to be already equipped with: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG.Build provides the following mixins: + - BiNearRing_of_AddMonoid +HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr + - A : Type + - one : A + - mul : A -> A -> A + - mulrA : associative mul + - mulr1 : left_id one mul + - mul1r : right_id one mul + - mulrDl : left_distributive mul add + - mulrDr : right_distributive mul add +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: add is an operation of structure AddMonoid + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: add comes from mixin AddMonoid_of_TYPE + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddAG.sort is a canonical projection + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.sort has the following canonical values: + - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) + - Z +HB: AddAG.sort is a coercion from AddAG to Sortclass + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: Z is canonically equipped with structures: + - AddMonoid + AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) +HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +Toplevel input, character 15: +> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: +HB: unable to locate +Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) diff --git a/tests/about.v.out.19 b/tests/about.v.out.19 new file mode 100644 index 000000000..3ac71cc29 --- /dev/null +++ b/tests/about.v.out.19 @@ -0,0 +1,142 @@ +HB: AddMonoid_of_TYPE is a factory + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE operations and axioms are: + - zero + - add + - addrA + - add0r + - addr0 +HB: AddMonoid_of_TYPE requires the following mixins: +HB: AddMonoid_of_TYPE provides the following mixins: + - AddMonoid_of_TYPE +HB: AddMonoid_of_TYPE.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: +HB: AddMonoid_of_TYPE.Build provides the following mixins: + - AddMonoid_of_TYPE +HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 + - S : Type + - zero : AddMonoid.sort S + - add : S -> S -> S + - addrA : associative add + - add0r : left_id 0%G add + - addr0 : right_id 0%G add +HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.type characterizing operations and axioms are: + - addNr + - opp +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring +HB: AddMonoid.type is a structure + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: AddMonoid.type characterizing operations and axioms are: + - addr0 + - add0r + - addrA + - add + - zero +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring +HB: Ring_of_AddAG is a factory + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG operations and axioms are: + - one + - mul + - mulrA + - mulr1 + - mul1r + - mulrDl + - mulrDr +HB: Ring_of_AddAG requires the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG provides the following mixins: + - BiNearRing_of_AddMonoid +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: Ring_of_AddAG.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG.Build requires its subject to be already equipped with: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG.Build provides the following mixins: + - BiNearRing_of_AddMonoid +HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr + - A : Type + - one : A + - mul : A -> A -> A + - mulrA : associative mul + - mulr1 : left_id one mul + - mul1r : right_id one mul + - mulrDl : left_distributive mul add + - mulrDr : right_distributive mul add +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: add is an operation of structure AddMonoid + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: add comes from mixin AddMonoid_of_TYPE + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddAG.sort is a canonical projection + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.sort has the following canonical values: + - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) + - Z +HB: AddAG.sort is a coercion from AddAG to Sortclass + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: Z is canonically equipped with structures: + - AddMonoid + AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) +HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +Toplevel input, character 15: +> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: +HB: unable to locate +Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) diff --git a/tests/about.v.out.20 b/tests/about.v.out.20 new file mode 100644 index 000000000..3ac71cc29 --- /dev/null +++ b/tests/about.v.out.20 @@ -0,0 +1,142 @@ +HB: AddMonoid_of_TYPE is a factory + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE operations and axioms are: + - zero + - add + - addrA + - add0r + - addr0 +HB: AddMonoid_of_TYPE requires the following mixins: +HB: AddMonoid_of_TYPE provides the following mixins: + - AddMonoid_of_TYPE +HB: AddMonoid_of_TYPE.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: +HB: AddMonoid_of_TYPE.Build provides the following mixins: + - AddMonoid_of_TYPE +HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 + - S : Type + - zero : AddMonoid.sort S + - add : S -> S -> S + - addrA : associative add + - add0r : left_id 0%G add + - addr0 : right_id 0%G add +HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.type characterizing operations and axioms are: + - addNr + - opp +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring +HB: AddMonoid.type is a structure + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: AddMonoid.type characterizing operations and axioms are: + - addr0 + - add0r + - addrA + - add + - zero +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring +HB: Ring_of_AddAG is a factory + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG operations and axioms are: + - one + - mul + - mulrA + - mulr1 + - mul1r + - mulrDl + - mulrDr +HB: Ring_of_AddAG requires the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG provides the following mixins: + - BiNearRing_of_AddMonoid +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: Ring_of_AddAG.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG.Build requires its subject to be already equipped with: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid +HB: Ring_of_AddAG.Build provides the following mixins: + - BiNearRing_of_AddMonoid +HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr + - A : Type + - one : A + - mul : A -> A -> A + - mulrA : associative mul + - mulr1 : left_id one mul + - mul1r : right_id one mul + - mulrDl : left_distributive mul add + - mulrDr : right_distributive mul add +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). +HB: add is an operation of structure AddMonoid + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: add comes from mixin AddMonoid_of_TYPE + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddAG.sort is a canonical projection + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.sort has the following canonical values: + - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) + - Z +HB: AddAG.sort is a coercion from AddAG to Sortclass + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: Z is canonically equipped with structures: + - AddMonoid + AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) +HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) +Toplevel input, character 15: +> HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: +HB: unable to locate +Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) diff --git a/tests/compress_coe.v.out b/tests/compress_coe.v.out index a958681b6..3e72d0064 100644 --- a/tests/compress_coe.v.out +++ b/tests/compress_coe.v.out @@ -1,3 +1,8 @@ +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 => {| diff --git a/tests/compress_coe.v.out.16 b/tests/compress_coe.v.out.18 similarity index 93% rename from tests/compress_coe.v.out.16 rename to tests/compress_coe.v.out.18 index 0d249e432..a958681b6 100644 --- a/tests/compress_coe.v.out.16 +++ b/tests/compress_coe.v.out.18 @@ -1,4 +1,4 @@ -Datatypes_prod__canonical__compress_coe_D = +Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| D.sort := D.sort D * D.sort D'; @@ -17,5 +17,4 @@ fun D D' : D.type => |} |} : D.type -> D.type -> D.type - Arguments Datatypes_prod__canonical__compress_coe_D D D' diff --git a/tests/compress_coe.v.out.19 b/tests/compress_coe.v.out.19 new file mode 100644 index 000000000..a958681b6 --- /dev/null +++ b/tests/compress_coe.v.out.19 @@ -0,0 +1,20 @@ +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' diff --git a/tests/compress_coe.v.out.20 b/tests/compress_coe.v.out.20 new file mode 100644 index 000000000..a958681b6 --- /dev/null +++ b/tests/compress_coe.v.out.20 @@ -0,0 +1,20 @@ +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' diff --git a/tests/err_instance_nop.v.out b/tests/err_instance_nop.v.out index 756fc7f93..167663615 100644 --- a/tests/err_instance_nop.v.out +++ b/tests/err_instance_nop.v.out @@ -1,3 +1,5 @@ -Toplevel input, character 155: +Toplevel input, character 0: +> HB.instance Definition _ : M nat := M.Build nat. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] diff --git a/tests/err_instance_nop.v.out.18 b/tests/err_instance_nop.v.out.18 new file mode 100644 index 000000000..756fc7f93 --- /dev/null +++ b/tests/err_instance_nop.v.out.18 @@ -0,0 +1,3 @@ +Toplevel input, character 155: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] diff --git a/tests/err_instance_nop.v.out.19 b/tests/err_instance_nop.v.out.19 new file mode 100644 index 000000000..756fc7f93 --- /dev/null +++ b/tests/err_instance_nop.v.out.19 @@ -0,0 +1,3 @@ +Toplevel input, character 155: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] diff --git a/tests/err_instance_nop.v.out.20 b/tests/err_instance_nop.v.out.20 new file mode 100644 index 000000000..756fc7f93 --- /dev/null +++ b/tests/err_instance_nop.v.out.20 @@ -0,0 +1,3 @@ +Toplevel input, character 155: +Warning: HB: no new instance is generated +[HB.no-new-instance,HB,elpi,default] diff --git a/tests/howto.v.out b/tests/howto.v.out index 5ac73ec37..0f685f26e 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -1,3 +1,8 @@ +Toplevel input, character 0: +> From Coq Require Import ZArith ssrfun ssreflect. +> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Warning: "From Coq" has been replaced by "From Stdlib". +[deprecated-from-Coq,deprecated-since-9.0,deprecated,default] HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE - AddAG_of_TYPE; BiNearRing_of_AddMonoid diff --git a/tests/howto.v.out.18 b/tests/howto.v.out.18 new file mode 100644 index 000000000..5ac73ec37 --- /dev/null +++ b/tests/howto.v.out.18 @@ -0,0 +1,55 @@ +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +The command has indeed failed with message: +HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_AddComoid + - AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddAG_of_AddComoid; Ring_of_AddAG + - AddAG_of_AddComoid; SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: nothing to do. diff --git a/tests/howto.v.out.19 b/tests/howto.v.out.19 new file mode 100644 index 000000000..5ac73ec37 --- /dev/null +++ b/tests/howto.v.out.19 @@ -0,0 +1,55 @@ +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +The command has indeed failed with message: +HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_AddComoid + - AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddAG_of_AddComoid; Ring_of_AddAG + - AddAG_of_AddComoid; SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: nothing to do. diff --git a/tests/howto.v.out.20 b/tests/howto.v.out.20 new file mode 100644 index 000000000..5ac73ec37 --- /dev/null +++ b/tests/howto.v.out.20 @@ -0,0 +1,55 @@ +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +The command has indeed failed with message: +HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_AddComoid + - AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddAG_of_AddComoid; Ring_of_AddAG + - AddAG_of_AddComoid; SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid +For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances +HB: nothing to do.