ghc-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.

cloud_download Downloads