Stream: new members

Topic: What's wrong with this notation?

Chris M (Apr 13 2020 at 05:08):

I've declared the notation notation '[' x 'ε' X ':' φ ']' := spec φ X (where I've just written  as ' to not mess with Zulip). Then when I write [ x ε X : x sub X ], I get all kinds of errors. How should I do what I want to do?

Edit: I get these errors:

unknown identifier 'x'
invalid expression starting at 50:19
command expected

Reid Barton (Apr 13 2020 at 06:41):

I don't know but you can use two backticks instead of one when you want to surround code containing a backtick.

Reid Barton (Apr 13 2020 at 06:42):

Perhaps Lean doesn't like having : taken away from it?

Chris M (Apr 13 2020 at 06:51):

I changed : to |, but that doesn't change the errors.

MWE?

Chris M (Apr 13 2020 at 06:54):

I googled "MWE", but the closest thing to this context is "Managed Work Environment", but I don't think that's what you meant.

Reid Barton (Apr 13 2020 at 06:55):

Oh yes, because x is not in scope

Kenny Lau (Apr 13 2020 at 06:55):

MWE = minimal working example

Kenny Lau (Apr 13 2020 at 06:56):

"working" is more important

Chris M (Apr 13 2020 at 06:59):

Ok.

definition N : Set := classical.some axiominfinity
definition myemptyset : Set := [x ε N | ¬x=x]


Reid Barton (Apr 13 2020 at 07:02):

You're trying to make the first argument treated as a binder. But this kind of notation syntax means x is an expression.

Chris M (Jun 08 2020 at 06:36):

@Reid Barton , sorry for the late reply. Corona disrupted my routine and I ended up only viewing this now.

Does the fact that x is treated as an expression mean that I can't use it multiple times in this notation? i.e. I can't reuse it within \phi?

How would I go about defining this kind of notation correctly within Lean?

Kevin Buzzard (Jun 08 2020 at 07:53):

There is some way of introducing binder notation in Lean 3 but it's a bit primitive. Look at the definition of notation like \Union` maybe for an example?

Last updated: May 06 2021 at 21:09 UTC