type Nat = Zero | Succ of Nat

let one = Succ Zero

let two = Succ (Succ Zero)

let three = Succ (Succ (Succ Zero))

let rec add x y = match x with

| Zero -> y

| Succ x -> Succ (add x y)

let rec mul x y = match y with

| Zero -> Zero

| Succ Zero -> x

| Succ y -> add x (mul x y)

let rec fac n = match n with

| Zero -> Succ Zero

| Succ x -> mul n (fac x)

open FsCheck

// Addition properties

Check.Quick (fun x y -> (add x y) = (add y x))

Check.Quick (fun x y z -> (add x (add y z)) = (add (add x y) z))

Check.Quick (fun x -> (add x Zero) = x)

// Multiplication properties

Check.Quick (fun x y -> (mul x y) = (mul y x))

Check.Quick (fun x y z -> (mul x (mul y z)) = (mul (mul x y) z))

Check.Quick (fun x -> (mul x one) = x)

## No comments:

Post a Comment