Commits

David Castro committed 859033a

mkQuant added in Z3.Lang.Monad.

  • Participants
  • Parent commits 803ca6c

Comments (0)

Files changed (1)

     , mkBound
     , mkForall
     , mkExists
+    , mkQuant
     , mkEq
     , mkCmp
     , mkFuncDecl
             -> Base.AST -> Z3 Base.AST
 mkExists = liftZ3Op5 Base.mkExists
 
+mkQuant :: Quantifier
+           -> [Base.Pattern]
+           -> [Base.Symbol] -> [Base.Sort]
+           -> Base.AST -> Z3 Base.AST
+mkQuant ForAll = mkForall
+mkQuant Exists = mkExists
+
 mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST
 mkEq Distinct = liftZ3Op2 Base.mkDistinct
 mkEq Neq      = mkNot <=< mkEq Eq