From stdlib's reflect to stdpp's Decision

reflect_bool_decide.v

Require Import iris.prelude.prelude.

Definition reflect_bool_decide b {P} : reflect P b -> Decision P.
  refine (
    match b with
    | true => λ r, left _
    | false => λ r, right _
    end).
  all: abstract by inversion r.
Defined.
#[global] Remove Hints Nat.eq_dec : typeclass_instances.
#[global] Instance nat_eqdec_reflect : EqDecision nat.
  refine (λ x y, reflect_bool_decide (Nat.eqb x y) _).
  abstract (exact: Nat.eqb_spec).
Defined.
Eval cbv in decide (5 = 6).
Eval cbv in bool_decide (5 = 6).
Eval cbv in bool_decide (5 = 5).