« Changelog History


ghc-typelits-natnormalise v0.6 Release Notes

Release Date: 2018-04-23 // about 6 years ago
    • Solving constraints with a-b will emit b <= a constraints. e.g. solving n-1+1 ~ n will emit a 1 <= n constraint.
      • If you need subtraction to be treated as addition with a negated operarand run with -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers, and the b <= a constraint won't be emitted. Note that doing so can lead to unsound behaviour.
    • Try to solve equalities using smallest solution of inequalities:
      • Solve x + 1 ~ y using 1 <= y => x + 1 ~ 1 => x ~ 0
    • Solve inequalities using simple transitivity rules:
      • 2 <= x implies 1 <= x
      • x <= 9 implies x <= 10
    • Solve inequalities using simple monotonicity of addition rules:
      • 2 <= x implies 2 + 2*x <= 3*x
    • Solve inequalities using simple monotonicity of multiplication rules:
      • 1 <= x implies 1 <= 3*x
    • Solve inequalities using simple monotonicity of exponentiation rules:
      • 1 <= x implies 2 <= 2^x
    • Solve inequalities using powers of 2 and monotonicity of exponentiation:
      • 2 <= x implies 2^(2 + 2*x) <= 2^(3*x)