def seek

bendtorch-core@0.1.0.0 · src/storage/api.bend:646

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

646def seek(+n: Nat, +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) ->
647  {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(20n, n, 0n, 1n, Nat.is_le(n, 1n))), n) == True{} : Bool}:
648  seek_bounds(20n, n, 0n, 1n, Nat.is_le(n, 1n), {==}, {==}, {==}, limit, positive)