def i64_p

bend-collections-laws-math@1.0.0.0 · proofs/math/random/wrappers.bend:64

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/spec/math/random/source.bend as SRC
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R

64def i64_p(-S: Data, p: W.U64 & S) -> {SW.value(R.fst(W.U64, S, R.low63(S, p))) == C.low(63n, SW.value(SRC.fst64(S, p))) : Nat}:
65  match p:
66    case Tuple{x, s}:
67      match x:
68        case W.U64{+l, +h}:
69          low63_v(l, h)