def ckp.is1

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

import Base

49def ckp.is1(+n: Nat) -> Type:
50  match n:
51    case 0n:
52      Unit
53    case 1n+p:
54      match p:
55        case 0n:
56          Empty
57        case 1n+q:
58          Unit