Re: [isabelle] RC5: Syntactic class bit_operations is gone

> order. Such a bundle will only work if the conflicting theory that
> > fixes the syntax in the typeclass is also loaded. 
> I don't get this point.  What is the »conflicting theory«?

A theory that defines a bundle for its syntax, starting with
no_notation ... to erase potential conflicting syntax, automatically
depends on the theory declaring the conflicting syntax, even if they
are logically independent. Otherwise, the user will be responsible to
do such a declaration at the merge point of two theories declaring
conflicting syntax.

> So, the bundle seems the way to go for now.  Since there is some
> rationale to put the most important bit operations into HOL-Main, I
> once
> thought to organize all infix syntax on bits in bundles anyway, to
> not
> clutter the syntactic space of HOL-Main.  If this is once
> accomplished
> after the release, the infix syntax is completely free.

Also, the bundling approach prevents you from using the same syntax for
the two related concepts, e.g., I can no longer write the statement: 

width a = width b ==> int_of (a AND b) = int_of a AND int_of b
for a b :: ll_word

In my solution, I now went for introducing a similar looking syntax,
i.e., a llAND b. But this approach will lead to cluttering the syntax
space with many variations of the same syntax, just b/c you cannot
share it where it would feel natural to share.

It seems like there is no fits-everything solution to this question


> Cheers,
> 	Florian

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