ListLen.hs

module ListClone () where

import Language.Haskell.Liquid.Prelude

make2d :: a -> Int -> Int -> [[a]]
make2d x n m = clone (clone x n) m

clone :: a -> Int -> [a]
clone x n
  | n == 0
  = []
  | otherwise 
  = x : (clone x (n-1))



-- check [] = [liquidAssertB True]
-- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss

chk :: [[a]] -> Bool
chk [] = liquidAssertB True
chk (xs:xss) =
  case xss of 
   (xs1:xss1) -> let n = length xs in liquidAssertB (length xs1 == n) && chk xss
   []         -> liquidAssertB True

fooL  = [[1, 1, 3], [2, 2, 5]]
fooL1 = let f = make2d n0 n1 n2 in f
    where n0 = 0
          n1 = 2
          n2 = 3
propL = chk fooL1
prop  = chk fooL