Aya是一种编程语言和证明助手，专为形式化数学和类型导向编程而设计。
Aya的类型系统具有类似于Arend的同源性(homotopical)特征、重叠但汇合的模式匹配以及对定义等式(definitionalequalities)的抽象。
目前Aya正在积极开发中，下面是关于它的部分特性：
依赖类型，包括pi类型、sigma类型等Arend-ishinterval类型，用于定义HoTT 路径类型并通过计算证明规则性包含 first-match 语义的模式匹配重叠和顺序无关的模式……
点击空白处退出提示
评论