# Zulip Chat Archive

## Stream: lean4

### Topic: Theorem Names

#### François G. Dorais (Mar 31 2021 at 20:45):

Some time ago, there was a decision to snake_case theorems in Lean 4. That change is not complete yet but that's fine, there are more important things to do. I'm puzzled about the implications. For example, which of these is the correct Lean 4 theorem name:

```
theorem beq_iff_eq (a b : Bool) : a == b ↔ a = b := sorry
theorem beq_iff_Eq (a b : Bool) : a == b ↔ a = b := sorry
theorem beq_Iff_Eq (a b : Bool) : a == b ↔ a = b := sorry
theorem BEq_iff_Eq (a b : Bool) : a == b ↔ a = b := sorry
theorem BEq_Iff_Eq (a b : Bool) : a == b ↔ a = b := sorry
```

Perhaps this one is tricky because of the implicit coercion, but I would still like to know. (FWIW, my fave is #3 but I'd be fine with any one.)

#### Mario Carneiro (Mar 31 2021 at 20:46):

I think it is 3

#### Chris B (Mar 31 2021 at 20:51):

I got this from an earlier post by S. Ullrich lean4_naming.png , not sure if it's still good.

#### Chris B (Mar 31 2021 at 20:58):

I'm not sure how that applies actually. There's a theorem `succ_Eq_add_one (n : Nat) : succ n = n + 1`

and one called `mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b`

, the capitalization of `Eq`

is up in the air.

#### Leonardo de Moura (Mar 31 2021 at 21:00):

We are still experimenting with different styles for naming theorems.

#### Mario Carneiro (Mar 31 2021 at 21:00):

I would like `Eq`

to not be capitalized, but I see why it is in the current convention

#### Eric Wieser (Mar 31 2021 at 22:16):

What if all type names in `Prop`

were actually lower case, using the handwavy "well these are just like functions returning a bool" argument?

#### Eric Wieser (Mar 31 2021 at 22:17):

Not just in lemma names, but actually rename `Eq`

back to `eq`

etc

#### Mario Carneiro (Mar 31 2021 at 22:23):

I would support that, although that means changing `Bool.true`

back to `tt`

so that it doesn't clash with `True`

#### Eric Wieser (Mar 31 2021 at 22:34):

I can see why `tt`

might seem unsatisfying to a user using Lean only for data / "regular programming"

Last updated: May 07 2021 at 13:21 UTC