notation command

Stream: general

[Michael Beeson]

I am trying to set up Lean to check proofs in NF set theory. All you need to know about it is that it's a first-order
theory with set membership, pairing {a , b}, ordered pairs <a, b> etc. So my questions would apply more or less to
setting up any first-order theory inside Lean. I tried to use a notation command to tell the parser how to parse {a , b} and < a, b> but it didn't
work, and the manual is a little too terse on the subject. So, here's my non-working file. Can anyone tell me how to fix it?

universe u
set_option default_priority 100
reserve infix ∈ : 50
reserve infix ⊆ : 50
reserve infix ∪ : 50
reserve infix ∩ : 50
notation: { l:(foldr , (a, b), } ) := 1
notation: ⟨ l:(foldr , (a, b), ⟩ ) := 1
class nf_model (α : Type u) :=
variable {α : u}
section nf_model
variables nf_model:α
variables x,y,z,u,v,a,b,R,S:α
(extensionality: ∀ {M:α }, ∀ a,b,x (x ∈ a ↔ x ∈ b) → a=b))
(binary_union: ∀ {M : α}, ∀ x (x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b))
(intersection: ∀ {M:α}, ∀ x (x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b))
(complement: ∀ {M:α}, ∀ x (x ∈ c(a) ↔ ¬ x ∈ a))
(implication: ∀ {M:α}, ∀ x (x ∈ imp(a,b) ↔ (x ∈ a → x ∈ b)))
(emptyset: ∀ {M:α}, ∀ x(¬ x ∈ \phi))
(pairing: ∀ {M:α}, ∀ x y z (x ∈ {a,b} ↔ (x = a ∨ x = b)))
(ordered_pairs: ∀ {M:α}, ∀ x y (⟨ x, y ⟩ = {x,{x,y}}))
(Vdef: ∀ {M:α}, ∀ x ( x ∈ V))
(relation_definition: ∀ {M:α}, Rel(X) ↔ ∀ z(z ∈ X → ∃ a,b (z =⟨ a, b⟩ )))
(Cartesian_product: ∀ {M:α}), ∀ x,y,u (u ∈ x × y ↔ ∃ a,b (a ∈ x ∧ b ∈ y ∧ u = ⟨ a,b \rangle))
(domain: ∀ {M:α}), ∀ R (Rel(R) → ∀ x(x ∈ dom(R) ↔ ∃ y(⟨ x, y ⟩ ∈ R))))
(inverse_relation: ∀ {M:α}), ∀ R (Rel(R) → ∀ x,y (⟨ x,y ⟩ ∈ inv(R) ↔ ⟨ y,x ⟩ ∈ R)))
(join: ∀ {M:α} ∀ R,S (Rel(R) ∧ Rel(S) → ∀ x ( x \in join(R,S) \iff
\exists a,b,c (x = ⟨ a,c ⟩ ∧ ⟨ a,b ⟩ \in R ∧ ⟨ b,c ⟩ \in S))
(equality_relation: ∀ {M:α} ∀ x( x ∈ eq ↔ ∃ z(x = ⟨ z, z⟩ )))
(subset_definition: ∀ {M:α} ∀ x,y (x ⊆ y ↔ ∀ z(z ∈ x → z ∈ y)))
(subset_relation: ∀ {M:α} ∀ x,y (⟨ x, y ⟩ ∈ subset ↔ x ⊆ y))
(union: ∀ {M:α} ∀ x,y (x ∈ union(y) ↔ ∃ z (z ∈ y ∧ x ∈ z)))
(singleton_image: ∀ {M:α} ∀ R(Rel(R) → ∀ x,y (⟨ x, y ⟩ ∈ SI(R) ↔ ∃ a,b(x = {a,a} ∧ y = {b,b} ∧ ⟨ a,b ⟩ ∈ R)))
end nf_model

[Reid Barton]

I suggest you start by not trying to use notation. Also, you can enclose Lean code on Zulip between ```lean and ``` .

[Reid Barton]

There are some other issues, like variable and section can't appear after class ... := like that.

[Reid Barton]

Mainly though you seem to be missing a specification of what ∈ should mean, like (elem : α -> α -> Prop) or something.

[Reid Barton]

And similarly for { , }