poi 0.18.0

A pragmatic point-free theorem prover assistant
Documentation
=== Domains and Partial Functions ===

A partial function is a function where the input is constrained in some way.
According to Path Semantics, this changes the identity of the function.
Therefore, one should think about partial functions as 'different' functions.

For example: `and(a, a)`. Type it and see what happens.

In `and(a, a)`, the input of `and` is constrained implicitly.
Poi reduces this first to `and{eq}(a)(a)` by adding `eq` as domain constraint.
This turns `and` into a partial function `and{eq}`.

Now, the identity of the `and` function has changed into another function.
Poi uses the rule `and{eq} => fstb` to reduce this expression further.
In the end, the expression `and(a, a)` is reduced to just `a`.