Arithmetic Made Difficult

Under construction. I don’t know exactly what this is yet. Links that don’t exist are my to-do list.

  1. Arithmetic Made Difficult
  2. Functions
  3. Booleans
  4. Set Combinators
  5. \(\mathbb{N}\)
  6. \(\mathsf{Lists}(A)\)
  7. Binary Trees
    • Type
      • Trees
      • Leaf and Fork
    • Recursion Operators
    • Arithmetic
  8. Fixed Radix Numeral Systems
    • CarryBase
    • PlusBase
    • TimesBase
  9. List of Arithmetics
    • On Boring and Repetitive Proofs
    • Partial and Total Orders
      • Sorted
      • Insertion Sort
      • Merge Sort
      • Lex and Friends
      • Chains
    • Semigroups and Monoids
      • Sproduct
      • Mproduct
    • Lattices
    • Semirings
  10. Streams

The old idea that there was no reasoning in Arithmetic is dead; the idea that the general axioms have no place in Arithmetic is no longer held by a progressive teacher… J.B.F. Showalter in “Arithmetic Made Easy”, 1897

Beware of bugs in the above code; I have only proved it correct, not tried it. Donald Knuth in “Notes on the van Emde Boas construction of priority deques: An instructive use of recursion”, 1977


Do not seek the footsteps of the wise; seek what they sought.

Matsuo Bashō (松尾芭蕉), from 「柴門の辞」 “Words by a Brushwood Gate”