Re: [isabelle] quotient over record type



On Sat, Feb 16, 2013 at 4:40 AM, John Wickerson <jpw48 at cam.ac.uk> wrote:
> 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".

The problem here is that "my_record" is really just a type
abbreviation for "unit my_record_ext".

(Question for the other Isabelle developers: How is an ordinary user
supposed to discover what abbreviations like this stand for?)

I expect that the declaration should work with the "my_record_ext" type.

- Brian





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