Re: [isabelle] locales & category theory
On Thu, 16 Apr 2009, Benedikt.AHRENS at unice.fr 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