decidable - リーンは、ステートメントが決定可能であることを確認できないと不平を言っています

Question

次の数量パーツを定義しようとしています:

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)

しかし、エラーが発生します

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

Hdecp のおかげで (pi p) が実際に決定可能であることをリーンに認識させるにはどうすればよいでしょうか?

Answer 1

edit : エラボレータは、定義のコンテキストで利用可能である限り、実際にはインスタンスを完全に単独で推論できます。

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)

---

元の答え（インスタンスがより複雑な仮説を持っている場合でも有用です）：

への明示的な呼び出しを避けたい場合は、インスタンスiteをローカルに導入できます。decidable

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