def ckp.nz1

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

import Base

60def ckp.nz1(-k: Nat, +e: {1n+1n+k == 1n : Nat}) -> Empty:
61  %e : ckp.is1(_)
62  Unit{}