[isabelle] Quotient Type Definition: Map and Relator

Dear quotient type experts,

When defining

  quotient_type 'a Q = "'a T" / "R" <proof>

for some existing type T and an equivalence relation R, I see two

  No map function defined for T. This will cause problems later on. 

  Generation of a parametrized correspondence relation failed.
  Reason:  No relator for the type "T" found.

What are the problems that these warnings allude to, and how can I
provide a map function and a relator to avoid them?

I have been browsing the documentation and examples, but with limited
insight so far.


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