with W_Pred; use W_Pred; package body FZ_Pred is --------------------------------------------------------------------------- -- Fundamental Predicate Operations on FZ (finite integers) --------------------------------------------------------------------------- -- 1 iff N == 0 (branch-free); else 0 function FZ_ZeroP(N : in FZ) return WBool is A : WBool := 1; begin for i in N'Range loop A := A and W_ZeroP(N(i)); end loop; return A; end FZ_ZeroP; pragma Inline_Always(FZ_ZeroP); -- 1 iff N is odd function FZ_OddP(N : in FZ) return WBool is begin return W_OddP(N(N'First)); end FZ_OddP; pragma Inline_Always(FZ_OddP); end FZ_Pred;