Type Theory & Functional Programmingに出てきたCoinductive typeのintro ruleに少し悩んだので. Coinductiveは最大不動点の形でかけるような型. 例えばStream(無限リスト)はP X = N × Xの時のPの最大不動点である. テキストにはCoinductiveのintro規則と計…