Email Gateway (Aug 19 2022 at 09:28): Email Gateway (Aug 19 2022 at 09:28):From: Peter Lammich <lammich@in.tum.de>
Hi all,
Refering to Isabelle2012 and also the current development version
(Changeset: eb7b59cc8e08)
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.
If this "feature" of interfering term and sort syntax is intended, I
propose renaming the div-typeclass, such that a user can again refer to
it without nasty no_notation or whatever workarounds.
Email Gateway (Aug 19 2022 at 09:28):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC