def sp.disc

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:141

import Base

141def sp.disc(n: Nat) -> Type:
142  match n:
143    case 0n:
144      Empty
145    case 1n+p:
146      Unit