Re: [isabelle] Parameterized Types?

Dear Robert,

what you require are dependent types, but these are not supported by Isabelle. Instead, we propagate the use of "locales" for formalisations of algebra. See the main trunk of session HOL-Algebra.

Quotient rings have not been formalised in this framework (neither have quotient fields, which you could get also with type classes), so this would be a welcome contribution.


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