<commit_before>/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>

Excluded middle + Hilbert implies every proposition is decidable.
-/
import logic.axioms.prop_complete logic.axioms.hilbert
open decidable inhabited nonempty

theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
  (or.elim (em a)
    (assume Ha, nonempty.intro (inl Ha))
    (assume Hna, nonempty.intro (inr Hna)))

theorem prop_decidable [instance] (a : Prop) : decidable a :=
arbitrary (decidable a)<commit_msg>feat(library/data/axioms): add 'type_decidable'<commit_after>/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <NAME>

Excluded middle + Hilbert implies every proposition is decidable.
-/
import logic.axioms.prop_complete logic.axioms.hilbert data.sum
open decidable inhabited nonempty sum

theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
  (or.elim (em a)
    (assume Ha, nonempty.intro (inl Ha))
    (assume Hna, nonempty.intro (inr Hna)))

theorem prop_decidable [instance] (a : Prop) : decidable a :=
arbitrary (decidable a)

theorem type_decidable (A : Type) : A + (A → false) :=
match prop_decidable (nonempty A) with
| inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
| inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)
end
{'fraction_non_alphanumeric': 0.10335747202106649, 'fraction_numerical': 0.007899934167215274, 'mean_word_length': 4.846153846153846, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '355421', 'n_tokens_mistral': 533, 'n_tokens_neox': 499, 'n_words': 170}