def pd.ndisc
import bend-osdev-cbc@0.1.0.0/PROOF_padded.bend as PROOFPaddedimport Base
68def pd.ndisc(n: Nat) -> Type:
69 match n:
70 case 0n:
71 Empty
72 case 1n+p:
73 Unit
import bend-osdev-cbc@0.1.0.0/PROOF_padded.bend as PROOFPaddedimport Base
68def pd.ndisc(n: Nat) -> Type:
69 match n:
70 case 0n:
71 Empty
72 case 1n+p:
73 Unit