Infoview settings

Stream: general

[Martin Dvořák]

Can the following be set (i.e., already available as optional settings) in the Infoview?

(1) I would like to see pairs written in ⟨x, y⟩ as all other constructors are. There are too many meanings of ( ) in Lean.

(2 ) Instead of (foo fun x => bar) I want to see foo (fun x => bar). Similarly, when it is a the end of the expression, instead of foo fun x => bar I want to see foo (fun x => bar) despite of the redundancy.

(3) I would like multiple funs not to be collapsed. Instead of fun a b => I would like to see fun a => fun b =>.

(4) I would like to see quantifiers without parentheses, i.e., ∀ i : ι, baz instead of ∀ (i : ι), baz.

[Eric Wieser]

These sound like pretty-printer settings, unless you're asking for UI in the infoview to change them

[Eric Wieser]

Most of those sound controversial as defaults (though obviously being able to adjust them for your own use is reasonable), but I do like the idea of (4)

[Martin Dvořák]

Thanks for the keyword! Now, do such pretty-printer settings exist?

[Eric Wieser]

I doubt it very much

[Eric Wieser]

But you can maybe write your own delaborator

[Martin Dvořák]

Just to clarify, I wasn't calling for making them default.

[Eric Wieser]

(1) amounts to disabling a built in delaborator, so should hopefully be possible

[Martin Dvořák]

My current workflow in bigger proofs is to repeatedly:
(1) make a step (like rw for example);
(2) write a show line to make sure the goal is really what I think it is, without having to rely on my interpretation of what the Infoview shows me.

Needless to say, my current workflow is pretty slow.

[Martin Dvořák]

Eric Wieser said:

(1) amounts to disabling a built in delaborator, so should hopefully be possible

Won't it result in Prod.mk x y instead?

[Martin Dvořák]

My life has significantly improved when I learnt I could do things like this:

package vcsp {
  moreServerOptions := #[⟨`autoImplicit, false⟩, ⟨`pp.structureInstances, false⟩]
}

I am now wondering how much can be achieved just by adding the right settings to my lakefile.

[Martin Dvořák]

PS: I guess (3) and (4) should go hand-in-hand as they both should address both fun and quantifiers.

[Martin Dvořák]

Eric Wieser said:

Most of those sound controversial as defaults (though obviously being able to adjust them for your own use is reasonable), but I do like the idea of (4)

Speaking of defaults, would you agree that ∀ a : α, ∀ b : β, R a b looks better than ∀ (a : α) (b : β), R a b (the current)?

[Notification Bot]

6 messages were moved from this topic to #general > emojis for voting by Johan Commelin.