@hackage / PeanoWitnesses

GADT type witnesses for Peano-style natural numbers.

Latest0.1.0.0

About

Metadata

  • Last updated , by kwf
  • License BSD-3-Clause

  • Maintained by: kenny.foner@gmail.com

  • Lottery factor: 0

Links

Installation

Readme

Witnesses for Peano naturals are unary natural numbers paired with a natural number type index. These terms act as witnesses of a particular natural; we can recover the type information by examining the terms.