Digits

A digit is simply a buffer of one to four values.

We build simple functional predicates on digits for use in specifications.

We now define addition of an element to the left of a digit.

It has become a little more interesting here, as we define our first function. We can add to a digit if and only if it is not already full. So, we require the argument digit to be accompanied by a proof that it is not full. We will use it to prove that the last branch is inaccessible ; we use the notation ! ('bang') to denote inaccessible program points, which are points where False can be proved. Note that we can pattern-match on d as if it was just a digit: properties have no influence on code, only on proofs.

The generated obligation (figure \ref{fig:}) is easily solved, as we have a contradiction in the context: both ~ full d and d = Four _ _ _ _ are present. We can define in a similar fashion addition on the right and the various accessors on digits (head, tail, last and liat). From now on we will omit the proof scripts used to solve obligations.