Decidable predicates

Stream: new members

[Martin Dvořák]

How can I say that pred has to be decidable in a way that is less awkward to write in Lean?

def f (pred : ℕ → Prop) [∀ x : ℕ, decidable (pred x)] (n : ℕ) : list ℕ :=
if pred n then [n] else []

[Anne Baanen]

You can use the docs#decidable_pred abbreviation:

def f (pred : ℕ → Prop) [decidable_pred pred] (n : ℕ) : list ℕ :=
if pred n then [n] else []