[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
warnings:

  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.

Best,
Tjark






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