On 08/05/15 21:40, d...@axiom-developer.org wrote:
There exists a few mathematical axiom statements in the category book
(Volume 10.2), associated with each category (look at SemiGroup for
example). The intention is to decorate all of the categories and
domains with mathematical axioms which can
I had actually had something similar in one of OpenAxiom's branch.
On Sat, May 9, 2015 at 3:37 AM, Martin Baker ax87...@martinb.com wrote:
On 08/05/15 21:40, d...@axiom-developer.org wrote:
There exists a few mathematical axiom statements in the category book
(Volume 10.2), associated with
Martin,
If you are using COQ then why not just map the COQ library entries into
the Axiom categories?
So if we take part of the base library here:
https://coq.inria.fr/library/Coq.Arith.Mult.html#
So the appropriate Axiom category could have an entry like:
Zero property
Lemma mult_0_r : forall
