Re: [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]

On Sun, 3 Jan 2016, Florian Haftmann wrote:

The quite recent de-ASCII-fication of symbols produced a collateral
damage, illustrated with the following snippet:

	theory Foo
	imports Main

	term "INFIMUM A (Îx. f x x)"

The problem is that we had the tradition to add (and remove) pretty
lattice syntax by need (cf. also theory Lattice_Syntax in HOL-Library),
falling back to ASCII syntax by default.

I've recovered the former behaviour in -- it relies on the order of syntax declarations. I.e. with Main HOL with ~~/src/HOL/Library/Lattice_Syntax.thy prints proper symbols, without the extra import it prints the old ASCII syntax.

The overall situation of syntax variants is a bit complex. I started the inititive to swap print modes "ASCII" vs. "xsymbols" after staring at a failed attempt to change the syntax of basic HOL connectives for more than 20min. In the longer run we should try to simplify this further.

I can forsee two solutions:
* retain ASCII syntax for INFIMUM, SUPREMUM;
* make pretty lattice syntax standard; this seems feasible since we have
syntactic type classes for all lattice operators anyway, but I guess
applications still contain definitions which do not match the type of
the polymorphic operators.

I've made a quick exploration of existing applications in Isabelle + AFP: variants of bot/top, inf/sup, Inf/Sup, INFIMUM/SUPREMUM with symbol syntax appear in more than one place, e.g. in HOLCF or ~~/src/HOL/Library/Boolean_Algebra.thy

So it looks like one of this HOL type class reform projects that can take weeks to get through -- i.e. something to be reconsidered after the release.


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