Readme.md

   1 # Description
   2
   3 This library enables to:
   4
   5 - Name types in a way that respect module boundaries
   6 (by not exporting the `data` constructor of those names).
   7 - Formulate logical propositions about those names.
   8
   9 As a library author, this enables to require and provide proofs of propositions checked at compile-time.
  10
  11 As a library user, this makes possible to prove propositions required to use that library.
  12
  13 # Acknowledgements
  14
  15 Based upon:
  16
  17 - Matt Noonan's [Ghosts of departed proofs](https://doi.org/10.1145/3242744.3242755),
  18 implemented in [gdp](https://hackage.haskell.org/package/gdp).