[isabelle] How to access a locale type parameter in a quotient type definition



Hi!

Consider the following attempt of a locale definition:

    locale example =
      fixes R :: "['a, 'a] ⇒ bool"
      assumes is_equivalence: "equivp R"
    begin
    
    quotient_type Q = 'a / R
    
    end

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,
Wolfgang





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