【函数语言程序设计】4
- 定义函数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【关系的性质】