Email Gateway (Aug 18 2022 at 13:23): Email Gateway (Aug 18 2022 at 13:23):From: Benedikt.AHRENS@unice.fr
Hello,
I am an Isabelle beginner and interested in the development on category
theory on
http://afp.sourceforge.net/browser_info/devel/HOL/Category/
.
My long term goal is to extend this library a bit.
The code is more or less self-explaining, but I have one question:
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.
locale category =
fixes CC (structure)
assumes dom_object [intro]:
"f : Ar ==> Dom f : Ob"
When you answer, please put me in CC, since I haven't subscribed to the
list yet.
Thanks a lot in advance,
ben
Email Gateway (Aug 18 2022 at 13:24):From: Makarius <makarius@sketis.net>
On Thu, 16 Apr 2009, Benedikt.AHRENS@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
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf
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.
Makarius
Last updated: May 03 2024 at 04:19 UTC