Re: [isabelle] Gcd and algebraic structures

Hi Jose,

> Defining a gcd in an arbitrary ring could be cumbersome working with
> structures represented by type classes. Nevertheless, we are mainly
> interested in working on principal ideal rings, where any two elements
> have a gcd. Hence, gcd would be a total function, and appropriate for a
> type class representation. We just wanted to take the chance to
> implement some additional Abstract Algebra (commutative rings, integral
> domains) in a proper way (including operations such as gcd), but maybe
> we will have to reshape this goal.

ok, this sounds indeed that you should go for type classes.  In case,
others can then use work and generalize it.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.