j
k
j a
j l
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a) data Z data S a
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
I thought I was getting this, but this part is confusing. What exactly does declaring "data Z" do?
Back to the thread
Back to the list