Re: [isabelle-dev] infix line breaking
I’d be in favour! Larry > On 23 Feb 2019, at 15:07, Makarius wrote: > > It might be better to introduce a proof-local version of 'abbreviation'. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
On 23/02/2019 12:25, Lawrence Paulson wrote:
> Which reminds me: I define such abbreviations all the time, using “let”.
> Could let-abbreviations be folded upon printing?
>
>> On 23 Feb 2019, at 09:10, Manuel Eberl wrote:
>>
>> I for one almost always do
>>
>> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
It might be better to introduce a proof-local version of 'abbreviation'.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
Which reminds me: I define such abbreviations all the time, using “let”. Could
let-abbreviations be folded upon printing?
Larry
> On 23 Feb 2019, at 09:10, Manuel Eberl wrote:
>
> I for one almost always do
>
> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
>
> in such cases, perhaps occasionally combined with a
>
> note [simp] = G_def [symmetric]
>
> at least during the "exploratory" stage of Isar proof writing.
>
> Without that, statements and proof obligations in HOL-Algebra become
> totally unreadable in my experience.
>
> Manuel
>
>
> On 22/02/2019 17:20, Lawrence Paulson wrote:
>> The pretty printing of infix operators looks pretty terrible in the presence
>> of large terms.
>>
>> I’d like to propose having infix operators breaking at the start of the line
>> rather than at the end. Any thoughts?
>>
>> Larry
>>
>> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0)
>> {pp}) {} (nsphere 0) {} r
>> d =
>>hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere
>> 0) {nn}) {} r
>> (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
I for one almost always do
define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
in such cases, perhaps occasionally combined with a
note [simp] = G_def [symmetric]
at least during the "exploratory" stage of Isar proof writing.
Without that, statements and proof obligations in HOL-Algebra become
totally unreadable in my experience.
Manuel
On 22/02/2019 17:20, Lawrence Paulson wrote:
> The pretty printing of infix operators looks pretty terrible in the presence
> of large terms.
>
> I’d like to propose having infix operators breaking at the start of the line
> rather than at the end. Any thoughts?
>
> Larry
>
> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0)
> {pp}) {} (nsphere 0) {} r
>d =
> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere
> 0) {nn}) {} r
>(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
On 22/02/2019 17:20, Lawrence Paulson wrote: > The pretty printing of infix operators looks pretty terrible in the presence > of large terms. > > I’d like to propose having infix operators breaking at the start of the line > rather than at the end. Any thoughts? Recall this recent thread on that (and many other infix-related cans of worms): https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07670.html Changing arrangements from many decades ago always takes a bit longer than expected, and one needs to try hard to get a result that is significantly better than the status-quo. We have require 2 full release cycles just to get the relative simple reform of (+) and (*) through (with a fully convincing result). From my side, the following two reforms are on the top of the stack of further moves: (1) eliminate most (or all) ASCII replacement syntax with the help of the "isabelle update" tool, e.g. ":" vs. "\" (2) get ==> out of the infix topic for most practical purposes, by printing goal states in Isar notation (fixes/assumes/shows or fix/assume/show or show/if/for). For the coming release I merely see (1) happening really soon: the "isabelle update" tool belongs to certain newly introduced infrastructure that deserves proper consolidation. (It is time to start thinking about which already open threads should be closed for the release.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
The point is the line breaking. Look at the occurrence of d before the =. This
applies to all infix operators, not just relations.
Larry
> On 22 Feb 2019, at 17:10, Tobias Nipkow wrote:
>
> We had already discussed this and decided that for "=", "<=" etc it makes
> sense.
>
> I find that the wrong associativity can be much more of a killer than where
> the infix op is placed.
>
> Tobias
>
> On 22/02/2019 17:20, Lawrence Paulson wrote:
>> The pretty printing of infix operators looks pretty terrible in the presence
>> of large terms.
>> I’d like to propose having infix operators breaking at the start of the line
>> rather than at the end. Any thoughts?
>> Larry
>> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0)
>> {pp}) {} (nsphere 0) {} r
>>d =
>> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere
>> 0) {nn}) {} r
>>(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
We had already discussed this and decided that for "=", "<=" etc it makes sense.
I find that the wrong associativity can be much more of a killer than where the
infix op is placed.
Tobias
On 22/02/2019 17:20, Lawrence Paulson wrote:
The pretty printing of infix operators looks pretty terrible in the presence of
large terms.
I’d like to propose having infix operators breaking at the start of the line
rather than at the end. Any thoughts?
Larry
inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp})
{} (nsphere 0) {} r
d =
hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
(hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0)
{nn}) {} r
(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] infix line breaking
The pretty printing of infix operators looks pretty terrible in the presence of
large terms.
I’d like to propose having infix operators breaking at the start of the line
rather than at the end. Any thoughts?
Larry
inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp})
{} (nsphere 0) {} r
d =
hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
(hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0)
{nn}) {} r
(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
