def un.nz

bend-osdev-u32@0.1.0.0 · PROOF.bend:1023

import Base

1023def un.nz(x: Nat) -> Type:
1024  match x:
1025    case 0n:
1026      Empty
1027    case 1n+p:
1028      Unit