def sp.disc

bend-osdev-cbc@0.1.0.0 · PROOF.bend:96

import Base

96def sp.disc(n: Nat) -> Type:
97  match n:
98    case 0n:
99      Empty
100    case 1n+p:
101      Unit