BitTree.nonempty_metadata_ok: def of mylsm-lsm-store@0.3.2.0
Import: import mylsm-lsm-store@0.3.2.0/src/BitTree.bend as BitTree
Lines 245-252 of mylsm-lsm-store@0.3.2.0/src/BitTree.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.3.2.0/src/BitTree.bend&start_line=245&end_line=252

import Base
import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/math/pow2.bend as Pow2

def nonempty_metadata_ok(root: WordTree, +words: Nat, +capacity: Nat, +height: Nat) -> Bool:
  Bool.and(
    Nat.is_gt(words, 0n),
    Bool.and(
      Nat.is_le(words, capacity),
      Bool.and(
        Nat.is_eq(capacity, Pow2.pow2t(height)),
        shape_ok(height, root))))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_gt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.3.2.0/src/BitTree.bend&name=WordTree
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.3.2.0/src/BitTree.bend&name=shape_ok