Documentation

The Plus type family provides a function that adds two type-level natural numbers. This function is implemented by induction on the first argument --- a fact that one should be aware of when using it in function signatures.

The Plus type family provides a function that subtracts two type-level natural numbers. This function is implemented by induction on both arguments, with the base case being when the second argument is Zero.