Aya是一种编程语言和证明助手，专为形式化数学和类型导向编程而设计。
Aya的类型系统具有类似于Ared的同源性(homotopical)特征、重叠但汇合的模式匹配以及对定义等式(defiitioalequalities)的抽象。
目前Aya正在积极开发中，下面是关于它的部分特性：
依赖类型，包括pi类型、sigma类型等Ared-ishiterval类型，用于定义HoTT 路径类型并通过计算证明规则性包含 first-match 语义的模式匹配重叠和顺序无关的模式……
点击空白处退出提示
Aya 形式化数学编程语言开源项目
我要开发同款
2022年08月03日技术信息
开源地址
https://github.com/aya-prover/aya-dev/授权协议
MIT
作品详情
功能介绍
Aya 是一种编程语言和证明助手，专为形式化数学和类型导向编程而设计。 Aya 的类型系统具有类似于 Arend 的同源性 (homotopical) 特征、重叠但汇合的模式匹配以及对定义等式 ...
声明：本文仅代表作者观点，不代表本站立场。如果侵犯到您的合法权益，请联系我们删除侵权资源！如果遇到资源链接失效，请您通过评论或工单的方式通知管理员。未经允许，不得转载，本站所有资源文章禁止商业使用运营!
评论