Resources-about-z3.md

@@ -9,3 +9,21 @@ Various resources found while trying to understand z3 better:
 - https://stackoverflow.com/questions/15758601/for-all-quantifier-in-z3
 - https://github.com/mrexodia/z3-haskell (git repository for the `Z3.Monad` module)
 - https://hackage.haskell.org/package/z3-4.1.1/docs/Z3-Monad.html (docs for `Z3.Monad`)
+
+## Z3.Monad mkForall
+
+```haskell
+-- | Create a forall formula.
+--
+-- The bound variables are de-Bruijn indices created using 'mkBound'.
+--
+-- Z3 applies the convention that the last element in /xs/ refers to the
+-- variable with index 0, the second to last element of /xs/ refers to the
+-- variable with index 1, etc.
+mkForall :: Context
+          -> [Pattern]  -- ^ Instantiation patterns (see 'mkPattern').
+          -> [Symbol]   -- ^ Bound (quantified) variables /xs/.
+          -> [Sort]     -- ^ Sorts of the bound variables.
+          -> AST        -- ^ Body of the quantifier.
+          -> IO AST
+```
\ No newline at end of file