def Nat.disc_z

lawful-arrays@0.1.0.0 · proof_base.bend:68

import Base

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