[Agda] Fin n -> Fin n extensional?
Andrés Sicard-Ramírez
asr at eafit.edu.co
Wed Feb 18 17:34:41 CET 2015
On 18 February 2015 at 11:20, Aaron Stump <aaron-stump at uiowa.edu> wrote:
> No wait, I spoke too soon. That type says that for any n, for any functions
> f and g, and for any input x, if f x equals g x then f equals g. That seems
> very strong. It is saying if the functions have the same output on any
> particular input x, then they are equal. I would have thought you meant:
>
> fin-ext : (n : ℕ)(f g : Fin n → Fin n) → ((x : Fin n) → f x ≡ g x) → f ≡ g
>
> Is that right?
I also wrote too soon :-) You are right.
--
Andrés
More information about the Agda
mailing list