ghc typelits presburger:内置类型级自然变量的Presburger算术求解器 源码

ghc-typelits-presburger和singletons-presburger -GHC插件,用于使用Presburger算术求解器改进类型级别的天然singletons-presburger 使用Presburger算术求解器,此monorepo中的程序包增强了GHC中的类型级特性。 粗略地说,它在编译时自动解决由加法,常数因子乘法和(不)等式表示的约束。 从0.3.0.0开始,与软件包的集成被分离到另一个插件 。 如果您需要处理singletons包裹,请改用它。 用法 将此软件包添加到您的构建依赖项中,并在程序顶部添加以下编译指示。 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} 从0.5开始,不需要在相关性上增加equational-reasoning 。 但是,如果要解决涉及equational-rea