def Nat.disc_z

minebender-game@1.0.0.0 · proof_base.bend:70

import Base

70def Nat.disc_z(n: Nat) -> Type:
71  match n:
72    case 0n:
73      Empty
74    case 1n+p:
75      Unit