Stream: new members
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
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):
|, but that doesn't change the errors.
Kevin Buzzard (Apr 13 2020 at 06:51):
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):
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