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):
nat -> bool case: let iff Turing machine halts in at most steps. If you could decide you'd decide the halting problem.
Kevin Buzzard (Dec 29 2020 at 18:22):
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