： 这是被称为（之一）德·摩根定律，并简单地指出的or否定荷兰国际集团的两个值必须与每个的否定相同。它已被证明很长一段时间，并且是LiquidHaskell's tutorial中的一个例子。我沿着教程以下，但未能得到下面的代码经过： -- Test.hs
module Main where
main :: IO()
main = return()
(==>) :: Bool -> B
我尝试写一些规格的Data.Ratio模块。到目前为止，我有： module spec Data.Ratio where
import GHC.Real
Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0}
我验证的代码是： {[email protected] di
我正在做一些使用液体哈斯克尔的实验来看看我可以用它做什么样的整齐的事情，并且我碰到了一堵墙。基本思想是我有一些功能需要访问令牌，在经过一段时间后过期。我试图看看如何使用liquid-haskell来确保令牌在将其传递到我的函数之前进行有效性检查。我在下面创建了一个最小工作版本，这说明了我的问题。当我对这个文件运行的液体，我得到以下错误： /tmp/liquidTest.hs:18:17-42: E