failed to synthesize DecidablePred

Stream: new members

[Ralf Stephan]

Why do I get this error? set_option diagnostics true makes no difference. Do I need to define PrimeBelow differently?

import Mathlib
set_option autoImplicit false
set_option diagnostics true
open Nat

def PrimeBelow (n p : ℕ) :=
  p ∈ (primesBelow n)

lemma count_PrimeBelow (n : ℕ) (hn : 2 < n) : count (PrimeBelow n) 2 = 0 := by
  sorry

failed to synthesize
  DecidablePred (PrimeBelow n)
use `set_option diagnostics true` to get diagnostic information

[Rida Hamadani]

Include this before your lemma

instance {n : ℕ} : DecidablePred (PrimeBelow n) := by
  unfold PrimeBelow
  infer_instance

[Ralf Stephan]

Thank you. So the definition needed the DecidablePred interface, and proven. I need to think more object-oriented.

[Eric Wieser]

Or use abbrev instead of def