Cicada（蝉语）是一门依赖类型编程语言，一个交互式定理证明器。
蝉语项目主要是为了帮助大众理解开发软件和研究数学事实上是同一类活动，实践这两项活动的人可以相互学习，并以非常好的方式相互帮助。
安装方式
npm install // Install dependencies
npm run build // Compile `src/` to `lib/`
npm run watch // Watch the compilation
npm run test // Run test
示例代码
将自然数定义为归纳数据类型 (inductive datatype)。
datatype Nat {
zero: Nat
add1(prev: Nat): Nat
}
function add(x: Nat, y: Nat): Nat {
return recursion (x) {
case zero => y
case add1(prev, almost) =>
add1(almost.prev)
}
}
评论