相关疑难解决方法(0)

我正在尝试解决LiquidHaskell 教程中的一些练习。所以，我这样写：

data List a = Nil | Cons a (List a) deriving (Show)                                                                                  
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List …