On this page:
Nat
z
s
nat->unary
nat-datum
add1
sub1
plus
mult
exp
square
nat-equal?
even?
odd?
6.12

3.4 Nat

This library defines the datatype Nat and several functions on them. Extends #%datum with nat-datum for handling natural number literals.

0 parameter type

Nat : Type

constructor

z : Nat

constructor

s : (-> Nat Nat)

The natural number datatype.

procedure

(nat->unary n)  syntax?

  n : syntax?
A phase 1 function that converts a natural number in decimal notation, as a syntax object, into a unary notation of the same natural number, as a syntax object.

procedure

(nat-datum syn f)  syntax?

  syn : syntax?
  f : procedure?
A phase 1 procedure for parsing natural number literals. Allows writing natural numbers in decimal notation. This module automatically updates #%datum using this procedure.

Examples:
> 0

(z)

> 10

(s (s (s (s (s (s (s (s (s (s (z)))))))))))

procedure

(add1 n)  Nat

  n : Nat
A more lispy name for s.

Examples:
> (s z)

(s (z))

> (add1 z)

(s (z))

procedure

(sub1 n)  Nat

  n : Nat
Return the predecessor of n, or z is n is z.

Example:
> (sub1 (s z))

(z)

procedure

(plus n m)  Nat

  n : Nat
  m : Nat
Add n and m.

Examples:
> (plus (s z) (s z))

(s (s (z)))

> (plus z (s z))

(s (z))

> (plus (s (s z)) (s z))

(s (s (s (z))))

procedure

(mult n m)  Nat

  n : Nat
  m : Nat
Multiply n and m.

Examples:
> (mult (s z) (s z))

(s (z))

> (mult z (s z))

(z)

> (mult (s (s z)) (s z))

(s (s (z)))

procedure

(exp m e)  Nat

  m : Nat
  e : Nat
Compute e to the mth exponent.

Examples:
> (exp (s z) (s z))

(s (z))

> (exp z (s z))

(s (z))

procedure

(square m)  Nat

  m : Nat
Compute m squared, i.e., (exp m (s (s z))).

Examples:
> (square z)

(z)

> (square (s (s z)))

(s (s (s (s (z)))))

procedure

(nat-equal? n m)  Bool

  n : Nat
  m : Nat
Return true if and only if n is equal to m.

Examples:
> (nat-equal? (s z) (s z))

(true)

> (nat-equal? z (s z))

(false)

procedure

(even? n)  Bool

  n : Nat
Return true if and only if n is even.

Examples:
> (even? (s z))

(false)

> (even? z)

(true)

> (even? (s (s z)))

(true)

procedure

(odd? n)  Bool

  n : Nat
Return true if and only if n is not even.

Examples:
> (odd? (s z))

(true)

> (odd? z)

(false)

> (odd? (s (s z)))

(false)