def lt_m

bend-kit-collections@0.1.4.1 · PROOF.bend:148

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws

148# lb lies below ub, when both exist.
149def lt_m(~K: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, ub: Maybe<&2, K>) -> Bool:
150  match ub:
151    case None{}:
152      True{}
153    case Some{u}:
154      Laws.above(~K, ~cmp, lb, u)

Uses (4)

Used by (3)