Zulip Chat Archive

Stream: general

Topic: local notation in message window

Patrick Massot (Apr 23 2018 at 14:37):

I have a local infix notation for an operation which is a local variable. Is there any hope to see Lean using this notation in the Lean messages window?

Patrick Massot (Apr 23 2018 at 15:31):

No idea, anyone? That would really help me.

Simon Hudon (Apr 23 2018 at 15:33):

I've struggled with that too. Recently, I had an idea but I haven't tried it yet. What's the type of your variable?

Patrick Massot (Apr 23 2018 at 15:34):

It's a composition law

Patrick Massot (Apr 23 2018 at 15:34):

op : R → R → R

Patrick Massot (Apr 23 2018 at 15:35):

local infix ` ◆ `:70 := op

Simon Hudon (Apr 23 2018 at 15:35):

Cool. Let's try this:

def my_op := op

local infix ` ◆ `:70 := my_op op

Patrick Massot (Apr 23 2018 at 15:36):

breaks everything :disappointed:

Simon Hudon (Apr 23 2018 at 15:38):

Was that not what you were going for?

Kenny Lau (Apr 23 2018 at 15:39):

def my_op := op

local infix ` ◆ `:70 := my_op

Kenny Lau (Apr 23 2018 at 15:39):

I think that's what he means

Patrick Massot (Apr 23 2018 at 15:40):

I understood he meant that

Patrick Massot (Apr 23 2018 at 15:40):

still breaks everything

Simon Hudon (Apr 23 2018 at 15:40):

is op a parameter or a variable?

Patrick Massot (Apr 23 2018 at 15:40):

variable

Simon Hudon (Apr 23 2018 at 15:41):

Are you inside a section?

Simon Hudon (Apr 23 2018 at 15:41):

Can you make it a parameter?

Patrick Massot (Apr 23 2018 at 15:41):

I meant no I'm not inside a section

Patrick Massot (Apr 23 2018 at 15:41):

I don't know about parameters

Simon Hudon (Apr 23 2018 at 15:42):

:laughing: I thought so. They're not great in Lean but sometimes you need them. Before I go there, can you show me the output of #check @my_op?

Patrick Massot (Apr 23 2018 at 15:44):

my_op : Π {R : Type u_3}, (R → R → R) → R → R → R

Kenny Lau (Apr 23 2018 at 15:44):

let's just forget that algebraic hierarchy

Simon Hudon (Apr 23 2018 at 15:48):

With a variable, if you use my_op somewhere, you need to provide an argument for each variable. With parameters, inside the section, the parameters are a bit like constant. Inside tactic proofs, they get a bit flaky though.

Patrick Massot (Apr 23 2018 at 15:48):

I don't see the relation between the hierarchy and the problem we discuss here

Simon Hudon (Apr 23 2018 at 15:48):

Try making op a parameter and wrap it and the related definitions in a section

Last updated: Dec 20 2023 at 11:08 UTC