[isabelle] How to access a locale type parameter in a quotient type definition
Consider the following attempt of a locale definition:
locale example =
fixes R :: "['a, 'a] ⇒ bool"
assumes is_equivalence: "equivp R"
quotient_type Q = 'a / R
Isabelle doesn’t accept the use of the type variable `'a` in the
quotient type definition, although it does accept referring to `'a` in
types. How can I define a quotient type for the type `'a`?
All the best,
This archive was generated by a fusion of
Pipermail (Mailman edition) and