~/jendhub

def bitw.ffs_set

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

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

226def bitw.ffs_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.ffs(n, w)) == nat.pos(A.bitw.ffs(n, w)) : Bool}:
227  match n:
228    case 0n:
229      {==}
230    case 1n+ +p:
231      match w:
232        case WCon{True{}, t}:
233          {==}
234        case WCon{False{}, +t}:
235          bitw.ffs_set.h(p, t, A.bitw.ffs(p, t), bitw.ffs_set(p, t))

Uses (8)

Used by (1)