What's wrong with this notation?

Stream: new members

[Chris M]

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]

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

[Reid Barton]

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

[Chris M]

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

[Kevin Buzzard]

MWE?

[Chris M]

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]

Oh yes, because x is not in scope

[Kenny Lau]

MWE = minimal working example

[Kenny Lau]

"working" is more important

[Chris M]

Ok.

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

[Reid Barton]

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]

@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]

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?