~/jendhub

def cnt_psm2

bendtorch@1.3.0.0 · PROOF.bend:207

import bendtorch@1.3.0.0/PROOF.bend as PROOF
import Base
import bendtorch@1.3.0.0/main.bend as T

207def cnt_psm2(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm2(kk, off, r))) == 1n+kk : Nat}:
208  match r:
209    case T.AS{a, +m}:
210      cnt_psm3(q, k, kk, off, T.pexp(kk, off, m, 0.0, Array.get(F32, a, off)))

Uses (11)

Used by (1)