Subtraction of natural numbers is non-total, and can result in negative numbers, which cannot be represented as a natural number. Most languages throw an except

Subtraction of natural numbers is non-total, and can result in negative numbers, which cannot be represented as a natural number. Most languages throw an exception, panic, etc. None of these are solutions I'm happy with. In Tao, natural numbers don't support subtraction but you can decrement them by pattern-matching as in this example, allowing the compiler to 'check your workings' and statically prove that your program can never result in underflows. In a similar vein, you can't index directly into a list (because indexing is a fallible operation). Instead, you must pattern-match on the list and explicitly handle the empty case (you can also write a utility function to do this for you like so) fn nth : Nat -> [A] -> Maybe A = | _, [] => None | 0, [x ..] => Just x \ n + 1, [.. tail] => tail->nth(n) Used like: [1, 2, 3]->nth(1) # Evaluates to `Some 2`