Zulip Chat Archive

Stream: new members

Topic: getting rid of lambda in the infoview


jachym simon (Apr 22 2022 at 16:24):

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 (Apr 22 2022 at 16:38):

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 (Apr 22 2022 at 16:47):

Turns out the @[simp] tag is not needed

jachym simon (Apr 22 2022 at 16:50):

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 (Apr 22 2022 at 16:55):

I had no idea that was legal syntax

Eric Wieser (Apr 22 2022 at 16:56):

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

Eric Wieser (Apr 22 2022 at 16:56):

Why not declare a has_sup instance?

Henrik Böving (Apr 22 2022 at 16:57):

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 (Apr 22 2022 at 17:01):

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

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

jachym simon (Apr 22 2022 at 17:09):

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 (Apr 22 2022 at 17:11):

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

jachym simon (Apr 22 2022 at 17:12):

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

jachym simon (Apr 22 2022 at 17:13):

Its defined as

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

jachym simon (Apr 22 2022 at 17:15):

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 (Apr 22 2022 at 17:18):

Try this:

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

jachym simon (Apr 22 2022 at 17:21):

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


Last updated: Dec 20 2023 at 11:08 UTC