小编SOA*_*OAP的帖子

我不太确定这个ZInt究竟在描述什么.

data Nat = Zero | S Nat
data ZInt = Z Nat Nat deriving Show

addZ :: ZInt -> ZInt -> ZInt
addZ (Z a b) (Z c d) = Z (add a c) (add b d)

with
add ::  Nat -> Nat -> Nat
add a Zero  = a
add a (S b) = S (add a b)

mult :: Nat -> Nat -> Nat
mult _ Zero  = Zero
mult a (S b) = add a (mult …

对于二叉树的数据类型,您可以编写如下内容:

data Tree a = Nil | Node a (Tree a) (Tree a)

因此,如果我想要包含树,而节点只有两个子节点,那么数据类型怎么可能看起来像？

鉴于这两个功能:

sumOne 0 = 0                                     --   I.a
sumOne m | m > 0 = sumOne (m-1) + m              --  II.a

endSum m = helpSum 0 m                           --   I.b
 where helpSum x 0 = x                           --  II.b
       helpSum x m | m > 0 = helpSum (x+m) (m-1) -- III.b

我们必须通过归纳证明sumOne = endSum.

所以我尝试过:

对于 n=0

sumOne 0=0 == endSum 0 = helpSum 0 0 = 0   True

假设:

sumOne m + k = helpSumm k m

诱导步骤:

-> m=m+1
helpSum …