[isabelle] Problem with implicit structure argument
I'm new to Isabelle and I need help with a problem regarding implicit
To learn Isabelle and since I would be interested in developing some
category theory in Isabelle, I'm trying to make some modifications to Greg
O'Keefe's AFP entry "Category theory using Isar and Locales" (the one
called "Category", not "Category2").
The essential modifications so far are related to two locales:
one_cat (in Functor.thy) and
into_set (in HomFunctor.thy).
In the original O'Keefe's code, these two locales introduce some kind of
"artificial" equations. E.g., the locale "one_cat" is obtained from
"two_cat" by adding an equation "BB = AA":
locale one_cat = two_cats +
assumes endo: "BB = AA"
I suspect that this approach was the only one available with some old
implementation of the locales machineries, but now we can do something
better by passing the appropriate parameters to the locale. This is what I
locale one_cat =
endo: two_cats AA AA
for AA :: "('o1,'a1,'m1) category_scheme" (structure)
Of course, the rest of the code has to be modified accordingly. I did part
of the work, but I'm now blocked by the following problem.
In the locale Yoneda (Yoneda.thy) the implicit structure argument is not
recognised anymore. For instance, I have to write ObâAAâ instead of simply
Ob. I do not understand why.
My code is available here
Thank you for you help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and