Middle argument

Stream: general

[Yaël Dillies]

Naming convention question! Consider f : ℕ → ℕ → ℕ → bool. How should these lemmas be called?

variables (a b c : ℕ)

example : f 0 b c = tt := sorry
example : f a 0 c = tt := sorry
example : f a b 0 = tt := sorry
example : f a b b = tt := sorry
example : f b a b = tt := sorry
example : f b b a = tt := sorry

I'm thinking _left, _middle,_right, _left, _middle,_right, but for example I already PRed docs#btw_refl_left_right.

[Yaël Dillies]

cc @Christopher Hoskin

[Christopher Hoskin]

Or possibly _mid as it's a bit shorter than _middle?

[Yaël Dillies]

Any more thoughts on this?