ghc-typelits-natnormalise

Version 0.7.4 revision 0 uploaded 2021-02-12T18:09:29.000Z by ChristiaanBaaij.

Package meta

Synopsis

GHC typechecker plugin for types of kind GHC.TypeLits.Nat

Description

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.

Author

Christiaan Baaij

Bug reports

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

Category

Type System

Copyright

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

Homepage

http://www.clash-lang.org/

Maintainer

christiaan.baaij@gmail.com

Package URL

n/a

Stability

n/a

Components

• lib:ghc-typelits-natnormalise
• test:test-ghc-typelits-natnormalise