Add prove of injectivity to Data.Fin.combine

[uzytkownik]

No description provided.

[MatthewDaggitt]

Thanks for the great PR! I've added a few comments.

[MatthewDaggitt]

Can we use the new with ... <- ... idiom instead of inspect? (see #1630 for an attempt to deprecate it.)

[uzytkownik]

combine-surjective : ∀ {n k} (x : Fin (n ℕ.* k)) → Σ[ y ∈ Fin n ] Σ[ z ∈ Fin k ] combine y z ≡ x
combine-surjective {n} {k} x with remQuot {n} k x in eq
... | y , z = y , z , (begin
  combine y z                       ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩
  uncurry combine (remQuot {n} k x) ≡⟨ combine-remQuot {n} k x ⟩
  x ∎)
  where open ≡-Reasoning

causes

Panic: uncaught pattern violation

What agda version I need to have?

[MatthewDaggitt]

Eek, that's scary. Agda 2.6.2 should be fine. If you're on that and the issue is still occuring, then I would open an issue on the main Agda repo with a cut-down example, and then I guess you'll need to switch back to inspect 👍

[uzytkownik]

I have 2.6.2.1. I will create an issue.

[MatthewDaggitt]

Thanks again for the PR!