Email Gateway (Aug 22 2022 at 12:03): Email Gateway (Aug 22 2022 at 12:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear syntax experts,
In HOL-Algebra, there are multiple cases where two structures are fixed in the same
context and declared as (structure) -- usually in the homomorphism locales. However, it
seems as if the second (structure) declaration cannot be used, because there are all the
\<^bsub>...\<^esub> annotations for the second structure. This is in line with the
implementation manual (Sect. 7.4.3), which states that "\<index>" always refers to the
first declared structure. This makes sense as it would not be clear in general which
variable to pick for the reference (although type checking might disambiguate things in
many practical cases).
IMO it would make sense to support constants that depend on several instances (for example
an operation on homomorphisms) and that thus should reference multiple structure
arguments. Unfortunately, I cannot even declare the mixfix syntax like in
"FOO\<index>\<index>"
because the parser complains about "Duplicate index arguments (\ı)". Is there a way to use
reference several implicit structures for a constant? If not, how hard would it be to
extend the index referencing to multiple references?
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC