~/jendhub

def ckp.ll

bend-osdev-acpi@0.1.2.0 · PROOF_checksum.bend:103

import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as PROOFChecksum
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

103def ckp.ll(+z: Nat) -> {U.U32Nat.low(8n, U.U32Nat.low(8n, z)) == U.U32Nat.low(8n, z) : Nat}:
104  UL.low_small(8n, U.U32Nat.low(8n, z), UL.low_lt(8n, z))

Uses (4)

Used by (1)