def absurd.nat

bend-osdev-algo@0.1.0.0 · PROOF.bend:32

import Base

32def absurd.nat(n: Nat) -> Type:
33  match n:
34    case 0n:
35      Empty
36    case 1n+p:
37      Unit