余帰納的型
#Fleeting_Notes
余帰納的型(coinductive type)
確認用
Q. 余帰納的型
メモ
Implementing a definitional (co)datatype package in Lean 4, based on quotients of polynomial functors
Data Types as Quotients of Polynomial Functors
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.6/LIPIcs.ITP.2019.6.pdf
調査用
Google.icon
余帰納的型(日)
Google.icon
Coinductive type(英)
Wikipedia.icon
余帰納的型 - Wikipedia(日)
余帰納的型(検索) - Wikipedia(日)
Wikipedia.icon
Coinductive type - Wikipedia(英)
Coinductive type(検索) - Wikipedia(英)