prime_eval.lean

namespace hidden

open classical
open decidable
local attribute [instance] prop_decidable

def divides (m n : ℕ) : Prop := ∃ k, m * k = n

instance : has_dvd ℕ := ⟨divides⟩

variables m n : ℕ

def prime (n : ℕ) : Prop := n ≥ 2 ∧ ∀ k, k ∣ n → k = 1 ∨ k = n 

#reduce prime 5
-- nat.less_than_or_equal 2 5 ∧ ∀ (k : ℕ), (∃ (k_1 : ℕ), nat.mul k k_1 = 5) → k = 1 ∨ k = 5

#eval to_bool $ prime 5
-- code generation failed, VM does not have code for 'classical.choice'

end hidden