有一切问题都可以问我. 这里是关于 Aya 的一个技术分享: https://docs.google.com/presentation/d/1jLUDV2SJvvuXzR9Oye0zuQS7CcgWJZWkZYP3i3T9FCY/edit#slide=id.p
5 个赞
补一下视频：102-千里冰封-高维编程语言 Aya_哔哩哔哩_bilibili
另外，在视频评论区提到的 数学教学工具，今天正好碰到这位朋友，打听到是基于 Lean 的 The Natural Number Game。除了他自己玩，也让小娃玩加法相关的。
看到 aya 仓库里一些issue 也提到 lean，不知两者目标和功能上有何异同呢？
1 个赞
冰冰来了 
1 个赞
Aya 更接近编程语言. 核心语言不使用 eliminator (而是底层就有模式匹配和递归功能), 并且有高维特性.
支持冰封（666）好久不见
1 个赞