~/jendhub

def AP.u32_inc

bend-osdev-array@0.1.0.1 · PROOF.bend:978

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
import bend-osdev-array@0.1.0.1/array.bend as A

978def AP.u32_inc(a: U32, d: Nat, h: {Nat.is_lt(1n+U32.to_nat(a), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
979  match a:
980    case U32{w}:
981      AP.inc(32n, w, d, h, hd)

Uses (9)

Used by (1)