I'm curious about a certain syntax involving "..". E.g., from the
agda-prelude:
data Fin : Nat → Set where
zero : ∀ ..{n} → Fin (suc n)
suc : ∀ ..{n} (i : Fin n) → Fin (suc n)
Where can I learn more about this? I didn't find it in the CHANGELOG or
the official User Manual. Was it discussed on this list perhaps?