~/jendhub

def bitw.fls_set

bend-osdev-algo@0.1.0.0 · PROOF.bend:300

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

300def bitw.fls_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.fls(n, w)) == nat.pos(A.bitw.fls(n, w)) : Bool}:
301  match n:
302    case 0n:
303      {==}
304    case 1n+ +p:
305      match w:
306        case WCon{b, +t}:
307          bitw.fls_set.h(p, t, A.bitw.fls(p, t), b, bitw.fls_set(p, t))

Uses (8)

Used by (1)