NAT-CONSTANT

Simply declares a single constant: nat-const. Used in NAT-PREFIX and derivatives. Spec is in: nat-prefix.re

NAT-PREFIX

Definitional extension of NAT-CONSTANT that defines an initial segement (prefix) of the natural numbers.

Sorts

• Nat-Prefix: the subsort of Nat determeined by in-prefix? (where (in-prefix? n) iff (lt n nat-const)).
• Nat-prefix-or-Error = Nat-Prefix + ()

Operations

• nat-const
• succ-nat-prefix
• pred-nat-prefix
• nat-to-nat-prefix-or-error
• last-in-prefix

Spec

Is in nat-prefix.re

Iteration/Higher Order

See numeric-specs , higher-order-specs and nat-ho.re

---

SpecWeb Index

Specs

---

---