Lean complains it can't see that a statement is decidable

Question

I'm trying to define the following quantity partn:

variable pi : nat -> Prop
variable (Hdecp : ∀ p, decidable (pi p))

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (if pi p then p^(mult p n) else 1)

but get the error

error: failed to synthesize placeholder
pi : ℕ → Prop,
n p : ℕ
⊢ decidable (pi p)

How can I help Lean recognize that (pi p) is indeed decidable thanks to Hdecp?

Answer 1

edit: The elaborator can actually infer the instance completely on its own, as long it's available in the definition's context:

variable (Hdecp : ∀ p, decidable (pi p))

include Hdecp
definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (if pi p then p^(mult p n) else 1)

---

original answer (still useful if the instance has more complex hypotheses):

If you want to avoid the explicit call to ite, you can locally introduce the decidable instance:

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n),
have decidable (pi p), from Hdecp p,
if pi p then p^(mult p n) else 1