- We define binary numbers (Bin) as sequences of Booleans.
Load ex3.epi into Epigram and complete the definitions of
- bone,bsix
- The binary representations of one and six.
- bin2nat
- Translates binary numbers to (Peano) natural numbers.
- nat2bin
- Translates natural numbers to binary.
- nat2natProp
- shows that bin2nat is inverse to nat2bin

- Introduce a representation of binary words of fixed length, i.e. define a type Word together with translations from and to Bin as defined above. Define addition for words (wadd).

The deadline for completing this coursework is Tuesday 6/12, 13:00. Once completed email the completed Epigram files to txa@cs.nott.ac.uk. There will be a short viva on your solution during the Tuesday lab after you have submitted it. Marks will be only be given after the viva.

Thorsten Altenkirch Last modified: Wed Nov 3 21:39:02 GMT 2004