[isabelle] Quotient Type Definition: Map and Relator
Dear quotient type experts,
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