Re: [isabelle] locales & category theory

On Thu, 16 Apr 2009, Benedikt.AHRENS at wrote:

What does the keyword "structure" in parentheses in the following code excerpt mean? I looked for it in the Isabelle tutorial (which does not cover locales, unfortunately) as well as in "Locales - a sectioning concept..." but could not find it.

This is briefly covered in the section on "Mixfix annotations" in the isar-ref manual, see

locale category =
 fixes CC (structure)
 assumes dom_object [intro]:
 "f : Ar ==> Dom f : Ob"

Declaring CC as "structure" makes it an implicit argument for "indexed syntax", cf. the definition of hom with syntax Hom in the same theory. Thus you can refer to "hom CC A B" as "Hom A B" in that context.


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