Agda-stdlib: Question on naming in Data.Fin.Base

[HuStmpHrrr]

consider two functions in
https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Base.agda#L65

fromℕ≤ : ∀ {m n} → m ℕ.< n → Fin n
fromℕ≤″ : ∀ m {n} → m ℕ.<″ n → Fin n

why are the names of these functions using ≤ instead of <? I know < is defined in terms of ≤ but still this is puzzling.

[MatthewDaggitt]

No idea, they predate me by quite a long way. I agree it's a little odd. Not sure if it's worth changing...

[HuStmpHrrr]

yeah, I am on the side to change them.

[JacquesCarette]

There's been a big push on consistency of naming, now's not the time to give up!