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

A type checker plugin for GHC that can solve *equalities* 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]

Versions [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 (info) |
---|---|

Change log | CHANGELOG.md |

Dependencies | base (>=4.9 && <5), ghc (>=8.0.1 && <8.4), ghc-tcplugins-extra (>=0.2), integer-gmp (==1.0.*) [details] |

License | BSD-2-Clause |

Copyright | Copyright © 2015-2016, University of Twente, 2017 , QBayLogic B.V. |

Author | Christiaan Baaij |

Maintainer | christiaan.baaij@gmail.com |

Category | Type System |

Home page | http://www.clash-lang.org/ |

Bug tracker | http://github.com/clash-lang/ghc-typelits-natnormalise/issues |

Source repo | head: git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git |

Uploaded | by ChristiaanBaaij at Sun Oct 22 19:47:56 UTC 2017 |

Distributions | Arch:0.6.2, LTSHaskell:0.6.2, NixOS:0.6.2, Stackage:0.6.2 |

Downloads | 9120 total (569 in the last 30 days) |

Rating | 2.25 (votes: 2) [estimated by rule of succession] |

Your Rating | |

Status | Docs available [build log] Last success reported on 2017-10-22 [all 1 reports] |

## Modules

[Index]

## Flags

Name | Description | Default | Type |
---|---|---|---|

deverror | Enables | Disabled | Manual |

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

## Downloads

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