Notation for the Lean InfoView

Stream: general

[Brandon Sisler]

Hey all, I was wondering how to alter the Lean Infoview so that it displays a nickname for a concept.
As an example if I wrote an inductive type

inductive BoolExpr where
...
  | val (b : Bool) -- special values, T or F
...

Then I might like BoolExpr.val true to be displayed in the infoview as T. Is there a way to do this? Thanks so much in advance!

[Mario Carneiro]

you can declare notation "T" => val true

[Brandon Sisler]

I did try notation:max "T" => BoolExpr.val true but the issue is that while I can use that notation in the Lean file, that the infoview still displays BoolExpr.val true.

[Shreyas Srinivas]

It tends to do that if you #eval

[Shreyas Srinivas]

Try using the #reduce command instead

[Brandon Sisler]

Wow, good tip, thanks!

[Mario Carneiro]

Oh good catch

[Kevin Buzzard]

Note that #reduce can be much slower than #eval because #reduce is done by the kernel as opposed to the (not formally verified) VM. At least this was the case in lean 3...

[Mario Carneiro]

#eval uses Repr to print the term, unlike in the tactic mode view or expected type view where you are looking at expressions directly

[Mario Carneiro]

You can also customize Repr to show T if you want

[Shreyas Srinivas]

I think it would be great if there was a crossover tactic command that evaluated like #eval and displayed using the unexpanders like #reduce. Customising Repr feels overkill

[Mario Carneiro]

You can use ToExpr instead of Repr, I posted code doing that here a little while ago

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Prettyprinting.20the.20result.20of.20an.20.23eval/near/403048023

[Mario Carneiro]

You will also want to use Mathlib.Tactic.DeriveToExpr

[Shreyas Srinivas]

Why is this in mathlib though? Sounds useful for other stuff too.

[Kyle Miller]

The story is that Scott tried to upstream it to Std, but that stalled out due to objections by Mario and Eric since there was the possibility of a Qq version in Std sometime in the future. https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/ToExpr.20derive.20handler/near/386191925

Mario's opinion back then was that ToExpr was "just some bootstrapping thing that no one else should need to care about" and that if you need the handler "you should either depend on mathlib or copy that handler into your project".

I'm hoping to potentially upstream it to Lean to enable using ToExpr instead of Repr for #eval as a default, since that would provide a nicer user experience (and we could fix the bugs in universe level handling in the core ToExpr instances), but I have no idea if or when this would happen.

[Mario Carneiro]

The fact that there are level bugs in some ToExpr instances especially contributes to this sense that it shouldn't be depended on too widely

[Kyle Miller]

The bug is that levels aren't handled at all

[Mario Carneiro]

exactly

[Mario Carneiro]

if those were fixed I'd feel better about having DeriveToExpr in std or core

[Kyle Miller]

They're fixed in DeriveToExpr

[Mario Carneiro]

yes, but then you have a mix of instances and only some combinations of them work

[Kyle Miller]

All the core instances are overridden in mathlib, but yes, it would be good if core handled these correctly. This requires upstreaming ToLevel to core

[Mario Carneiro]

they are overridden with instances which have more assumptions, I think that means the bad ones will still be used if those assumptions are not satisfied

[Kyle Miller]

Yes, that's a bug, and it would be good to remove the instance attribute from the core ones for the mathlib instances to be completely correct.

[Kyle Miller]

"Upstreaming to core" of course would mean fixing core's instances using ToLevel rather than monkeypatching.

[Kyle Miller]

Kyle Miller said:

Yes, that's a bug, and it would be good to remove the instance attribute from the core ones for the mathlib instances to be completely correct.

Correction: I already did remove the instance attribute from core instances, so there is no bug, assuming there have been no new ToExpr instances.

https://github.com/leanprover-community/mathlib4/blob/ce9ef8bea420e374f6daf1089ae6a2c8a7dcedd4//Mathlib/Tactic/ToExpr.lean

[Mario Carneiro]

does that actually work? I thought attribute removal is local only

[Kyle Miller]

Guess it doesn't, so correction correction, there's a bug.

I wonder if there's a way to make ToLevel more robust. I know one issue is that it can go off the rails if there are metavariables. In the following, α ends up specializing to α : Type 125.

import Mathlib.Tactic.ToExpr

variable (α : Type _) [Lean.ToExpr α]

#check Lean.ToExpr.toExpr ([] : List α)

[Mario Carneiro]

we would need to have a way to indicate that the universe is an outparam

[Mario Carneiro]

that doesn't seem likely in the near term so I would be inclined to just live with it

[Mario Carneiro]

I think this is another good example of a typeclass that wants to run custom logic

[Mario Carneiro]

I still think it was a bad idea to not make the typeclass system extensible in that way