[Agda] Fin n -> Fin n extensional?

Andrés Sicard-Ramírez asr at eafit.edu.co
Wed Feb 18 17:04:09 CET 2015


On 18 February 2015 at 10:51, Aaron Stump <aaron-stump at uiowa.edu> wrote:
> Sorry, but what does "functions at type (Fin n -> Fin n) are extensional"
> mean?

fin-ext : (n : ℕ)(f g : Fin n → Fin n)(x : Fin n) → f x ≡ g x → f ≡ g


-- 
Andrés


More information about the Agda mailing list