# ghc-typelits-natnormalise: GHC typechecker plugin for types of kind GHC.TypeLits.Nat

[ bsd2, library, type-system ] [ Propose Tags ]

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


Versions [RSS] [faq] 0.1, 0.1.1, 0.1.2, 0.2, 0.2.1, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.4.3, 0.4.4, 0.4.5, 0.4.6, 0.5, 0.5.1, 0.5.2, 0.5.3, 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, 0.7.5, 0.7.6 (info) CHANGELOG.md base (>=4.9 && <5), containers (>=0.5.7.1 && <0.7), ghc (>=8.0.1 && <8.11), ghc-tcplugins-extra (>=0.3.1), integer-gmp (==1.0.*), syb (>=0.7.1 && <0.8), transformers (>=0.5.2.0 && <0.6) [details] BSD-2-Clause Copyright © 2015-2016, University of Twente, 2017-2018, QBayLogic B.V. Christiaan Baaij christiaan.baaij@gmail.com Type System http://www.clash-lang.org/ http://github.com/clash-lang/ghc-typelits-natnormalise/issues head: git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git by ChristiaanBaaij at 2020-03-09T08:57:50Z Arch:0.7.6, LTSHaskell:0.7.6, NixOS:0.7.6, Stackage:0.7.6 25179 total (148 in the last 30 days) 2.25 (votes: 2) [estimated by Bayesian average] λ λ λ Docs uploaded by userBuild status unknown

## Modules

[Index] [Quick Jump]

## Manual Flags

NameDescriptionDefault
deverror

Enables -Werror for development mode and TravisCI

Disabled
Automatic Flags
NameDescriptionDefault

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

#### Maintainer's Corner

For package maintainers and hackage trustees

Candidates

[back to package description]

# ghc-typelits-natnormalise

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.

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}