def ndec

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:53

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

53# Mirror of an update at a Nat index (proof-level description of the new tree).
54# `left` is this node's branch decision (see ndec); passing it as a parameter
55# avoids matching on a computed value.
56def ndec(d: Nat, +j: Nat) -> Bool:
57  match d:
58    case 0n:
59      False{}
60    case 1n+q:
61      Nat.is_lt(j, SC.pow2(q))