New reduces and normalizations in Plugin for GCD, LCM, Min and Max

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver

Other

16 stars 9 forks source link

New reduces and normalizations in Plugin for GCD, LCM, Min and Max #9

Closed SkorikGG closed 6 years ago

SkorikGG commented 7 years ago

Is it possible to implement such type equalities as GCD m m ~ m, LCM m 1 ~ m , GCD m n ~ GCD n m, Min m n ~ Min n m?

christiaanb commented 7 years ago

The simple properties of GCD and LCM have been added. Also commutativity properties of Min, Max, GCD, and LCM have been added. Could you check if the implementation of those commutativity properties is sufficient for your use case? Things might not work if things are deeply nested and/or the equations inside Max etc. are complex.

christiaanb commented 6 years ago

Closing as solved, please reopen if the implementation is insufficient