Idris

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(项目)
(项目)
 
(未显示1个用户的6个中间版本)
第11行: 第11行:
  
 
==功能==
 
==功能==
 +
*[https://idris2.readthedocs.io/en/latest/tutorial/theorems.html Theorem Proving(定理证明)]
 +
*通过允许程序员描述对象语言的类型系统来帮助嵌入式 DSL 开发
 +
*Idris 2 is based on [https://bentnib.org/quantitative-type-theory.html Quantitative Type Theory (QTT)] 量化类型理论
  
 
==指南==
 
==指南==
  
 
==项目==
 
==项目==
*[[Coq]]
+
*[https://github.com/idris-lang Idris @ GitHub]
*[[Agda]]
+
*相似项目:[[Coq]], [[Agda]]
 +
 
 +
==文档==
 +
*[https://www.type-driven.org.uk/edwinb/papers/idris-qtt.pdf Idris 2: Quantitative Type Theory in Action]
  
 
==图集==
 
==图集==
第22行: 第28行:
 
==链接==
 
==链接==
 
*[http://idris-lang.org/ Idris 官网]
 
*[http://idris-lang.org/ Idris 官网]
*[https://github.com/idris-lang Idris @ GitHub]
 
  
 
[[category:programming language]]
 
[[category:programming language]]

2022年9月25日 (日) 16:50的最后版本

Wikipedia-35x35.png 您可以在Wikipedia上了解到此条目的英文信息 Idris Thanks, Wikipedia.

Idris programming language

目录

[编辑] 简介

Idris 是一个通用的依赖类型纯函数式编程语言,其类型系统与 Agda 以及 Epigram 相似。

Idris 语言具备堪与 Coq 媲美的交互式定理证明能力,自带 tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括可观的代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。

Idris 语言使用 Haskell 编写实现,采用 BSD licenses 许可证。

[编辑] 功能

[编辑] 指南

[编辑] 项目

[编辑] 文档

[编辑] 图集

[编辑] 链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱