def none_of

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:28

import Base
import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF

28def none_of(~T: Data, ~val: T -> Nat, +bad: Bool, +hb: {bad == True{} : Bool}, +r: T) -> {SF.mval(~T, ~val, F.opt(T, bad, r)) == None{} : Maybe<&2, Nat>}:
29  %Equal.sym(Bool, bad, True{}, hb) : {SF.mval(~T, ~val, F.opt(T, _, r)) == None{} : Maybe<&2, Nat>}
30  {==}