【函数语言程序设计】4

  1. 定义函数square,目的是计算给定自然数n的平方,但是不能用乘法运算。
Coq代码
Fixpoint square( n : nat ): nat :=
match n with
|0 => 0
|S n' => square n' + n' + n' + 1
end.

Compute (square 10).

运行截图

【学习】函数语言程序设计 文章被收录于专栏

函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】

全部评论

相关推荐

牛客771574427号:恭喜你,华杰
点赞 评论 收藏
分享
不愿透露姓名的神秘牛友
11-24 20:55
阿里国际 Java工程师 2.7k*16.0
程序员猪皮:没有超过3k的,不太好选。春招再看看
点赞 评论 收藏
分享
点赞 收藏 评论
分享
牛客网
牛客企业服务