[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 ...

----8<---------------------

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

----8<---------------------

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

Thanks,

John






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