# Zulip Chat Archive

## Stream: new members

### Topic: Custom notation inside structures

#### Kuba (May 18 2023 at 23:37):

Hi,

I have a structure whose constructor takes, among other things, a quaternary congruence relation and proofs of some of its properties as arguments. I would like to define a custom notation, so that I can write `a b ≅ c d`

instead of `congruence a b c d`

. However, if I use the `notation`

command and then try to use the newly defined notation, I get an error.

My code:

```
structure space where
(point_t : Type)
(congruence : point_t → point_t → point_t → point_t → Prop)
notation a b " ≅ " c d => space.congruence a b c d
(symmetry_of_congruence : ∀ a b : point_t, a b ≅ b a)
```

Error message (relating to the congruence symbol on the last line):

```
expected token
```

#### Chris Bailey (May 19 2023 at 04:19):

The parser won't let you declare notation inside a structure declaration. You would want to declare the notation beforehand somewhere in the syntax/macro/notation hierarchy. One way of doing it (someone can probably give you a more clean implementation):

```
set_option hygiene false in
macro a:term b:term " ≅ " c:term:max d:term : term => `(congruence $a $b $c $d)
structure space where
(point_t : Type)
(congruence : point_t → point_t → point_t → point_t → Prop)
(symmetry_of_congruence : ∀ a b : point_t, a b ≅ b a)
#print space
```

#### Eric Wieser (May 19 2023 at 05:58):

Does putting the notation command in `()`

help?

#### Eric Wieser (May 19 2023 at 05:59):

Oh nevermind, this is lean4

#### Kuba (May 22 2023 at 23:24):

Hmm, thanks for the answer, but I feel a bit queasy about disabling an option that has "hygiene" in its name. Does anyone know whether there is a cleaner way of doing this? I would have thought that my use case is a pretty common one. Or maybe the problem is with me using a lean structure here? What I am trying to achieve, is to describe a space made up of points and equipped with two relations that satisfy certain axioms. Both the points and the relations are primitive notions.

#### Reid Barton (May 23 2023 at 11:42):

Of course you can always manually expand the notation while defining the structure, and the worst that can happen is it may be hard to read/write.

#### Reid Barton (May 23 2023 at 11:42):

Sometimes it could also make sense to split the structure into two parts, and define the notation in between.

#### Chris Bailey (May 23 2023 at 13:55):

Kuba said:

Hmm, thanks for the answer, but I feel a bit queasy about disabling an option that has "hygiene" in its name. Does anyone know whether there is a cleaner way of doing this?

```
macro a:term b:term " ≅ " c:term:max d:term : term =>
`($(mkIdent `congruence) $a $b $c $d)
```

(This produces pretty much identical code, but if it makes you feel better to not write the word hygiene, go for it)

#### Kyle Miller (May 24 2023 at 10:01):

"Hygienic macros" refers to making sure that identifiers in a macro expansion do not accidentally refer to local variables -- here, you *do* want `congruence`

to refer to the local `congruence`

. Think of it not that your macro is dirty, but that the hygiene system doesn't understand what you're trying to do.

Since `congruence`

is the only literal identifier in your macro expansion, `set_option hygiene false`

will only has affect on the handling of that one identifier.

#### Kuba (May 24 2023 at 21:21):

I see, that makes sense. What I ended up doing was separating out the two relations as separate type classes and then having the axioms as a structure. This is what I ended up with (the code has grown a bit since I started):

```
set_option autoImplicit false
class Congruence (point_t : Type) where
(congruence : point_t → point_t → point_t → point_t → Prop)
notation:37 a:38 b:38 " ≅ " c:max d:38 => Congruence.congruence a b c d
class Betweennes (point_t : Type) where
(betweennes : point_t → point_t → point_t → Prop)
notation:37 a:38 " B " b:max c:38 => Betweennes.betweennes a b c
-- Five Segment Configuration
def FSC {point_t : Type} [Congruence point_t] [Betweennes point_t]
(a b c d : point_t) (a' b' c' d' : point_t) : Prop :=
b B a c ∧
b' B a' c' ∧
a b ≅ a' b' ∧
b c ≅ b' c' ∧
a d ≅ a' d' ∧
b d ≅ b' d'
structure TarskisAxioms (point_t) [Congruence point_t] [Betweennes point_t] where
(congruence_of_reversed : ∀ a b : point_t, a b ≅ b a)
(transitivity_of_congruence :
∀ a b p q r s : point_t, a b ≅ p q ∧ a b ≅ r s → p q ≅ r s)
(identity_axiom_for_congruence : ∀ a b c : point_t, a b ≅ c c → a = b)
(segment_extension_axiom :
∀ o p a b : point_t, ∃ q : point_t, p B o q ∧ p q ≅ a b)
(five_segment_axiom :
∀ a b c d a' b' c' d' : point_t,
FSC a b c d a' b' c' d' ∧ a ≠ b → c d ≅ c' d')
(identity_axiom_for_betweennes : ∀ a b : point_t, a B b b → a = b)
```

Does this approach make sense? I think this may be similar to how mathlib does it, but I only took a brief look. Also, how do you choose the precedence values? I think I managed to tune them by trial and error, but I am wondering if there is a recipe to follow.

Last updated: Dec 20 2023 at 11:08 UTC