decidable_eq with functions

Stream: new members

[Marcus Rossel]

Why is equality of functions not decidable?

[Johan Commelin]

Doesn't that depend on from where and to where the functions go?

[Kevin Buzzard]

import tactic

instance : decidable_eq (bool → bool) := by apply_instance

[Rob Lewis]

For the nat -> bool case: let $f_n(k) = T$ iff Turing machine $n$ halts in at most $k$ steps. If you could decide $f_n = \lambda k, F$ you'd decide the halting problem.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

[Eric Wieser]

I assume there is a docs#decidable_eq instance for arguments with fintype inputs and decidable_eq outputs?