Re: [isabelle] Questions about theories distributed with Isabelle

Hi Josh,

> First, the
> refers
> to type-classes disparagingly. Does the Isabelle community at large believe
> that "axiomatic type classes" cannot be "first-class citizens of the
> logic"? If so, I'd be interested to know *why* that's the case, but it's
> not required so don't spend too much time explaining.
> Second, many of the theories listed in HOL-Algebra are topically similar to
> theories included in HOL's Main. Why are they split out?

as a rule of thumb, there are basically two algebraic hierarchy
developments in HOL:

HOL-Main with type classes:
* implicit use due to type inference
* pragmatic and simple sharing between similar types
* explicit definitions
* directly executable
* …

HOL-Algebra with locales:
* explicit carrier – possibility to develop proper meta theory
* implicit definitions where possible
* suitable for mathematics

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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