ghc-typelits-extra-0.1.1: Additional type-level operations on GHC.TypeLits.Nat

Copyright(C) 2015, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellSafe
LanguageHaskell2010
Extensions
  • MonoLocalBinds
  • TypeFamilies
  • DataKinds
  • KindSignatures
  • ExplicitNamespaces

GHC.TypeLits.Extra

Description

Additional type-level operations on Nat:

A custom solver for the above operations defined is defined in GHC.TypeLits.Extra.Solver as a GHC type-checker plugin. To use the plugin, add the

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}

pragma to the header of your file.

Synopsis

Documentation

type family GCD x y :: Nat Source

Type-level greatest common denominator (GCD).

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

GCD 0 x = x 

type family CLog x y :: Nat Source

Type-level equivalent of:

clog x y = ceiling (logBase x y)

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

CLog 2 1 = 0