# Re: [isabelle] Record for module?

It seems that the reason for this is to use the additive \oplus notation
for module rather than \otimes. (Monoid uses \otimes, and it seems that
once the notation is chosen it cannot be changed.)

-Holden

2014-07-16 18:28 GMT+01:00 Holden Lee <hl422 at cam.ac.uk>:

> I need a record for a module but the *record module* in Module.thy
> actually defines a record for an algebra instead (an algebra has
> multiplication, a module does not) - so is a bit of a misnomer.
>
> record ('a, 'b) module = "'b *ring*" +
>   smult :: "['a, 'b] => 'b" (infixl "⊙ı" 70)
> [note it's "ring" not "monoid"]
>
> The *locale module* is correct but does not seem to have a record
> associated with it.
>
> I'm wondering whether I've missed it somewhere, or I need to define my
> own. If I do formalise it myself (by changing "ring" to "monoid" above)
> will it still be compatible with the locale module? As a side note, is it
> true that a record can only "inherit" from one other record (so that
> there's no way to have something like
>
> record ('a, 'b) Module = "('a ring)" + "('b monoid)" +
>   smult :: "['a, 'b] => 'b" (infixl "⊙ı" 70)
>
> that would encapsulate both a ring and module?)
>
> [I'm formalising vector spaces over an arbitrary field; a vector space is
> a module where the ring is a field.]
>
> (Thanks for all the helpful responses to my previous queries!)
>
> -Holden
>



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