Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
Code Sync · 5 则 HN 推荐
视频问答
可以让 AI 解释当前片段，或总结整部视频。如果回答附有时间戳，点击即可跳到对应片段。
试着问：这里讲的是什么意思？
需要用 Google 登录。确认前可查看最多会扣除多少积分。
Edwin Brady presents Idris 2, a rewrite of the Idris dependently typed language, and shows type-driven development in practice. The demos show the compiler filling in whole functions from their types.
HN 推荐的原因： HN points to it as a good introduction to Idris 2 and a striking demonstration of what dependent types enable.
“this looks like a good introduction” 阅读 HN 讨论 ↗