getting rid of lambda in the infoview

Stream: new members

[jachym simon]

Hey, i have defined an infix like this (the meaning is not important)

@[simp] local infix  ` ⊔ `: 90 := λ P Q: Form, (P ⇒ Q) ⇒ Q

I have set set_option trace.simplify.rewrite true. When simp uses anything with this infix, the infix is in the infoview written out as λ P Q: Form, (P ⇒ Q) ⇒ Q. Is there some way how to make lean print in the infoview P ⊔ Q instead?

[Kevin Buzzard]

I think "what simp does" and "notation" are two different things. What happens if you remove @[simp] and don't do the set_option?

[jachym simon]

Turns out the @[simp] tag is not needed

[jachym simon]

The problem is, that simp is doing crazy things while proving some lemmas and i wanted to know, what is it doing. So i have set set_option to see the steps it did, but since its using λ..., ... instead ⊔ in the infoview it is just a big mess i cant orient in.

[Eric Wieser]

I had no idea that was legal syntax

[Eric Wieser]

You need to give that operator a name for lean to pretty-print it, is my guess

[Eric Wieser]

Why not declare a has_sup instance?

[Henrik Böving]

If infix works the same here as it does in Lean 4 this notation does make sense since notation commands basically expand into parser declarations though tagging the parser itself with simp will of course not have the desired effect^^

[Reid Barton]

Maybe you would have more luck with (if I got the syntax right)

local notation P ` ⊔ `:90 Q:90 := (P ⇒ Q) ⇒ Q

[jachym simon]

Eric Wieser said:

Why not declare a has_sup instance?

This unfortunately works just half way for me. It prints nicely, but for some reason breaks some usages in lemmas i have in my code other things

[Eric Wieser]

Does Form have a le operator? Does it respect the rules of docs#semilattice_sup?

[jachym simon]

The Form is a type that represents logical formulas. It doesnt have le operator

[jachym simon]

Its defined as

  inductive Form : Type
  | p : ℕ → Form
  | imp : Form → Form → Form
  | neg : Form → Form

[jachym simon]

Reid Barton said:

Maybe you would have more luck with (if I got the syntax right)

local notation P ` ⊔ `:90 Q:90 := (P ⇒ Q) ⇒ Q

It seems this works the same way as the infix, but does not change the printing unfortunatelly

[Patrick Johnson]

Try this:

@[reducible] def f (P Q : Form) := (P ⇒ Q) ⇒ Q
local infix ` ⊔ `:90 := f

[jachym simon]

The has_sup instance actually works. I was confused, because it messed up the binding strength, so i had to add brackets to some places