Specware 4.1 Language Manual
PrevAppendix B. Inbuilts and Base LibrariesNext

Nat

Types

type Nat = {n : Integer | n >= 0}

type PosNat = {n : Nat | n > 0 }

Ops

Name Fixity Type Description
succ  Nat -> Nat successor
pred  Nat -> Integer predecessor
zero  Nat the natural number 0
one  Nat the natural number 1
two  Nat the natural number 2
posNat?  Nat -> Boolean yields false for 0, true otherwise
toString  Nat -> String converts natural number to string
show  Nat -> String same as toString
natToString  Nat -> String same as toString
natConvertible  String -> Boolean tests if string is representation of natural number
stringToNat  (String | natConvertible) -> Nat converts "convertible" string to natural number

PrevHomeNext
IntegerUpChar