[isabelle] quotient over record type

Dear Isabelle,

Does the Quotient package works with record types? I'm beginning to suspect that it doesn't, because when I type ...


record my_record = 
  foo :: "nat"
  bar :: "int"
declare [[mapQ3 my_record = (something,something_else)]]


... I get "Bad type name: my_record".



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