Re: [isabelle] Issue with typeclass-parsing: div-class cannot be specified



On Fri, 7 Dec 2012, Peter Lammich wrote:

I just found the following issue with type-class parsing:

term "a::'a::div"

*** Inner syntax error (line 5 of
"/home/lammich/devel/isabelle/Scratch.thy") at "div"
*** Failed to parse term


The same occurs for
 fixes a :: "'a::div"

and also for variations of the syntax like: "'a::{div}" or
"'a::{times,div}"


It seems to be the case that term-syntax influences sort syntax here:
 Adding a no_notation "div" (infixl "div" 70) solves the problem.

Term-syntax also influences type syntax, so
 typedecl div
 term "a::div"
has a simlar problem.

The error messages above use the correct terminology in speaking first about "inner syntax" in the generic sense. Terms, types, classes/sorts all share the same syntactic framework. Having a keyword that overlaps with identifier syntax, it is subtracted from it in the usual way. It has been like that in Isabelle in the past 20 years.

You can use Divides.div instead, as already done in several other places.


	Makarius





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