~/jendhub

def nonempty_metadata_ok

mylsm-lsm-store@0.3.2.0 · src/BitTree.bend:245

import mylsm-lsm-store@0.3.2.0/src/BitTree.bend as BitTree
import Base
import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/math/pow2.bend as Pow2

245def nonempty_metadata_ok(root: WordTree, +words: Nat, +capacity: Nat, +height: Nat) -> Bool:
246  Bool.and(
247    Nat.is_gt(words, 0n),
248    Bool.and(
249      Nat.is_le(words, capacity),
250      Bool.and(
251        Nat.is_eq(capacity, Pow2.pow2t(height)),
252        shape_ok(height, root))))

Uses (8)

Used by (1)