# Description

This library enables to:

- Name types in a way that respect module boundaries
(by not exporting the `data` constructor of those names).
- Formulate logical propositions about those names.

As a library author, this enables to require and provide proofs of propositions checked at compile-time.

As a library user, this makes possible to prove propositions required to use that library.

# Acknowledgements

Based upon:

- Matt Noonan's [Ghosts of departed proofs](https://doi.org/10.1145/3242744.3242755),
implemented in [gdp](https://hackage.haskell.org/package/gdp).