~/jendhub

def low_low

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:58

import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as Step
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

58def low_low(+k: Nat, +x: Nat) -> {C.low(k, C.low(k, x)) == C.low(k, x) : Nat}:
59  WW.low_fit(k, C.low(k, x), WW.low_fits(k, x))

Uses (4)

Used by (1)