def occurrences
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as Randimport Base
111def occurrences(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +v: V, xs: List<&2, A>) -> Nat:
112 match xs:
113 case Nil{}:
114 0n
115 case Con{+x, rest}:
116 Nat.add(b2n(rel(x, v)), occurrences(~A, ~V, ~rel, v, rest))
Uses (5)
Used by (7)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle:occ
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle:shuffle_perm
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle:range_occ
- bend-collections-laws-crypto@1.0.0.0/spec/crypto/random:Random.shuffle
- bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle:perm_perm
- …