| 11 | Notes: |

| 12 | * {{{(<=)}}} is a 2-parameter class (that's what we mean by the "kind" Prop), |

| 13 | * {{{(+)}}}, {{{(*)}}}, and {{{(^)}}} are type functions. |

| 14 | * Programmers may not provide custom instances of these classes/type-families. |

| 15 | |

| 16 | The operations correspond to the usual operations on natural numbers. |

| 17 | |

| 18 | |

| 19 | == Inverse Operations == |

| 20 | |

| 21 | Using the basic operations and GHC's equality constraints it is also possible to express |

| 22 | some additional constraints, corresponding to the inverses (when defined) of the above functions: |

| 23 | {{{ |

| 24 | Constraint | Alternative Interpretation | Example (x "input", y "output") |

| 25 | ---------------+-------------------------------+-------------------------------- |

| 26 | (a + b) ~ c | Subtraction: (c - b) ~ a | Decrement by 8: x ~ (y + 8) |

| 27 | (a * b) ~ c | Division: (c / b) ~ a | Divide by 8: x ~ (y * 8) |

| 28 | (a ^ b) ~ c | Log at base: Log a c ~ b | Log base 2: x ~ (2 ^ y) |

| 29 | (a ^ b) ~ c | Nth-root: Root b c ~ a | Square root: x ~ (y ^ 2) |

| 30 | }}} |

| 31 | |

| 32 | |

| 33 | |

| 34 | |