Re: [isabelle] Parameterized Types?
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