►Cur
▼3 Standard Library
3.1 Datum
3.2 Sugar
3.3 Bool
3.4 Nat
3.5 Dependent Pairs
3.6 Maybe
3.7 List
3.8 Equality
3.9 ASCII
3.10 Racket ASCII
3.11 Typeclass
On this page:
Nat
z
s
nat->unary
nat-datum
add1
sub1
plus
mult
exp
square
nat-equal?
even?
odd?
8.12
  top  contents    up   

3.4 Nat🔗ℹ

 (require cur/stdlib/nat) package: cur-lib
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))

(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))

odd?: unbound identifier in module

> (odd? z)

odd?: unbound identifier in module

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

odd?: unbound identifier in module

  top  contents    up