Zulip Chat Archive

Stream: general

Topic: Middle argument

Yaël Dillies (Jan 21 2022 at 06:57):

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 (Jan 21 2022 at 08:01):

cc @Christopher Hoskin

Christopher Hoskin (Jan 21 2022 at 08:15):

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

Yaël Dillies (Feb 03 2022 at 08:33):

Any more thoughts on this?

Last updated: Dec 20 2023 at 11:08 UTC