klagt sie nicht sehen können, dass eine Aussage entscheidbar ist

Question

Ich versuche, die folgende Menge partn zu definieren:

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) 

aber bekommen den Fehler

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

Wie kann ich helfen Lean erkennen dass (pi p) tatsächlich dank Hdecp entscheidbar ist?

Answer 1

bearbeiten explizit verwenden Hdecp erlaubt: vollständig die Instanz Der Ausarbeiter kann allein tatsächlich schließen, so lange es in der Definition der Kontext verfügbar ist:

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) 

---

ursprüngliche Antwort (noch nützlich, wenn die Instanz komplexere Hypothesen hat):

Wenn Sie den expliziten Aufruf ite vermeiden möchten, können Sie vor Ort einzuführen, um die decidable Beispiel:

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 

Answer 2

ich eine Lösung gefunden:

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (@ite (pi p) (Hdecp p) nat (p^(mult p n)) 1) 

, die ich in meinem if-the-sonst