!4#3320

Stream: PR reviews

[Jeremy Tan]

!4#3320 was created because of one of Eric's comments on !4#2450. I'd like a quick review so we can merge !4#2450 sooner

[Kevin Buzzard]

docs#fin.cast_succ_cast_lt

[Jeremy Tan]

@Kevin Buzzard in mathlib4 (currently):

@[simp]
theorem castSucc_cast_lt (i : Fin (n + 1)) (h : (i : ℕ) < n) : castSucc (castLt i h) = i :=
  Fin.eq_of_veq rfl
#align fin.cast_succ_cast_lt Fin.castSucc_cast_lt

@[simp]
theorem cast_lt_castSucc {n : ℕ} (a : Fin n) (h : (a : ℕ) < n) : castLt (castSucc a) h = a := by
  cases a; rfl
#align fin.cast_lt_cast_succ Fin.cast_lt_castSucc

[Jeremy Tan]

castLt is in the declaration, so castLt should be in the name too

[Kevin Buzzard]

Weekly reminder that I still have no understanding of the new naming convention

[Kevin Buzzard]

I thought "proof => mathlib3 style blah_blah_blah"

[Mario Carneiro]

I think it would be castSucc_castLt with that name

[Kevin Buzzard]

That's what the PR does

[Mario Carneiro]

although I think we're spelling it castLT and castLt is a mathportism

[Kevin Buzzard]

Kevin Buzzard said:

Weekly reminder that I still have no understanding of the new naming convention

[Jeremy Tan]

So should it be castLT everywhere?

[Mario Carneiro]

yeah

[Kevin Buzzard]

Is there anyone out there who can make a simple mathlib4 naming convention game? I'm serious.

[Mario Carneiro]

Mathlib.namingConvention_game

[Jeremy Tan]

@Mario Carneiro commit pushed