Two functions for converting a number into its binary representation, and converting a binary string into a number:
-- Converts a binary denotation into a nat
-- @param: binary denotation ( e.g. "0101")
-- @return: binarys nat representation
FUN binToNat : denotation -> nat
-- Converts a number (nat) into a binary denotation
-- @param: Number (nat)
-- @return: Binary representation as a denotation
FUN natToBin : nat -> denotation