params.hs

import Data.SBV

-- generate a model of 9 sInt8's that are always increasing and positive
-- I just named a0 below explicitly, but of course you can name any of
-- the parameters you want.
--
-- also see the functions: free/exists/forall/sBool/sBools/sInt8/sInt8s etc;
-- there's a pair (singular and plural) provided for each basic type SBV
-- supports.
tst = sat $ do as@(a0 : _) <- mapM free ['a' : show i | i <- [0..8]]
               let increasing []  = true
                   increasing [x] = true
                   increasing (x:y:rs) = x .< y &&& increasing (y:rs)
               constrain $ a0 .> (0::SInt8)
               return $ increasing as