Decidability of Prop-valued structure

Stream: lean4

[Mitchell Lee]

Hello, is there a clean way to prove that a Prop-valued structure is decidable, or to somehow use deriving to derive it? Here is a silly example:

structure IsBetweenThreeAndFive (n : Nat) : Prop where
  ge_three : 3 ≤ n
  le_five : n ≤ 5

instance : DecidablePred IsBetweenThreeAndFive := by
  sorry

[Yaël Dillies]

import Mathlib.Tactic.Common

@[mk_iff]
structure IsBetweenThreeAndFive (n : Nat) : Prop where
  ge_three : 3 ≤ n
  le_five : n ≤ 5

instance : DecidablePred IsBetweenThreeAndFive :=
  fun _ ↦ decidable_of_iff' _ (isBetweenThreeAndFive_iff _)

[Mitchell Lee]

Thanks!