~/jendhub

def lt_m.some

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

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

156def lt_m.some(
157  ~K: Data, ~cmp: K -> K -> Cmp, ub: Maybe<&2, K>, +k: K,
158  e: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}
159) -> {lt_m(~K, ~cmp, Some{k}, ub) == True{} : Bool}:
160  match ub:
161    case None{}:
162      {==}
163    case Some{u}:
164      e

Uses (5)

Used by (1)