law find_none

bend-osdev-algo@0.1.0.0 · LAWS.bend:255

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

255law find_none:
256  for xs: List<&2, U32>
257  for key: U32
258  for i: Nat
259  for x: U32
260  for s: {S.bsearch.sorted(xs) == True{} : Bool}
261  for e: {S.bsearch.find(xs, key) == None{} : Maybe<&2, Nat>}
262  for g: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
263  {U32.is_eq(x, key) == False{} : Bool}