[isabelle] Multiple (structure) arguments



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




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