« Home

實作 [tt-0003]

而 strictly positive 就是說，inductive family DD 自己不可以出現在 negative position

在 Agda 的文件中也有解釋：任何 constructor 都形如

(y1:B1)→⋯→(ym:Bm)→D(y_1 : B_1) \to \dots \to (y_m : B_m) \to D

而每個 BiB_i 都可以不提到 DD 或是形如

(z1:C1)→⋯→(zm:Cm)→D(z_1 : C_1) \to \dots \to (z_m : C_m) \to D

CjC_j 不可以等於 DD