Email Gateway (Aug 22 2022 at 12:09): Email Gateway (Aug 22 2022 at 12:09):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The quite recent de-ASCII-fication of symbols produced a collateral
damage, illustrated with the following snippet:
theory Foo
imports Main
begin
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 can forsee two solutions:
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 12:18):From: Makarius <makarius@sketis.net>
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
beginterm "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
http://isabelle.in.tum.de/repos/isabelle/rev/fefd79f6b232 -- 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.
Makarius
Email Gateway (Aug 22 2022 at 12:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
[...]
I have something in the pipeline for after release which will make this
all a little bit easier.
Florian
signature.asc
Last updated: Apr 19 2024 at 16:20 UTC