Agda-stdlib: Small change to inject≤

[xekoukou]

inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ {n = zero} zero ()
inject≤ {n = suc n} zero le = zero
inject≤ (suc i) (s≤s le) = suc (inject≤ i le)

https://agda.github.io/agda-stdlib/Data.Fin.Base.html#3219

This way, we avoid to need to pattern match on le , which can be hard to do on a proof, we would need to abstact over le so as to pattern match.

[gallais]

You could also use ≤-pred in the suc i case.

[xekoukou]

Yes, it is much better now :

inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ {n = zero} zero ()
inject≤ {n = suc n} zero le = zero
inject≤ {n = zero} (suc i) ()
inject≤ {n = suc n} (suc i) le = suc (inject≤ i (≤-pred le))

[MatthewDaggitt]

Sounds good.

[gallais]

Note that with 2.6.0 we should be able to leave out the impossible cases.

[xekoukou]

The same can be done to fromℕ≤ .
I can upload the changes now, or later after 2.6.0

[MatthewDaggitt]

Probably best to wait until after 2.6.0 and I reset the CHANGELOG

[andreasabel]

I think this should wait until 2.6.0.1 is out, see https://github.com/agda/agda/issues/3692. ;)

[MatthewDaggitt]

Fixed with 1690f69