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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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