## Stream: new members

### Topic: decidable_eq with functions

#### Marcus Rossel (Dec 29 2020 at 17:56):

Why is equality of functions not decidable?

#### Johan Commelin (Dec 29 2020 at 18:15):

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

#### Kevin Buzzard (Dec 29 2020 at 18:21):

import tactic

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


#### Rob Lewis (Dec 29 2020 at 18:21):

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 (Dec 29 2020 at 18:22):

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

#### Eric Wieser (Dec 29 2020 at 22:40):

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

Last updated: May 09 2021 at 20:11 UTC