A type checker plugin for GHC that can solve equalities and inequalities of types of kind Nat, where these types are either:

• Type-level naturals

• Type variables

• Applications of the arithmetic expressions (+,-,*,^).

It solves these equalities by normalising them to sort-of SOP (Sum-of-Products) form, and then perform a simple syntactic equality.

For example, this solver can prove the equality between:

(x + 2)^(y + 2)

and

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Because the latter is actually the SOP normal form of the former.

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.Normalise

Pragma to the header of your file.

---

[Skip to Readme]

Modules

[Index] [Quick Jump]

Flags

Manual Flags

Name	Description	Default
deverror	Enables `-Werror` for development mode and TravisCI	Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

• ghc-typelits-natnormalise-0.7.5.tar.gz [browse] (Cabal source package)
• Package description (as included in the package)

Maintainer's Corner

Package maintainers

• ChristiaanBaaij, QBayLogic

For package maintainers and hackage trustees

• edit package information

Candidates

• 0.5.4, 0.5.5, 0.5.6, 0.5.7, 0.5.8, 0.5.9, 0.5.10, 0.6, 0.6.1, 0.6.2, 0.7, 0.7.1, 0.7.2, 0.7.3, 0.7.4