Add section in README

examples/README.md

@@ -33,3 +33,24 @@ and pass it to the `--include` option of the `ortac qcheck-stm` command.
 The generated code can be found in `lwt_dllist_tests.ml`. You can run the test
 either with `dune runtest examples/` or by directly running the compiled
 executable that you will find in your `_build` directory.
+
+## `varray` library
+
+This is an example of a library exposing Functor. In order to test a Functor,
+it is necessary to instantiate it. The [`varray`](https://github.com/art-w/varray)
+library already exposes intantiation of its Functor. Here, we provide generated tests
+for two of them.
+
+The signature of the output of the Functor is originally placed in a `ml` file.
+`varray_sig.ml` is a copy of this file with some specifications. As Gospel
+doesn't process `ml` files, we extract the content of the module signature and
+place a copy in two files: `varray_spec.mli` and `varray_circular_spec.mli`,
+the former for the module exposed by `varray` as `Varray` and the latter for
+the module exposed by `varray` as `Varray.Circular`. The corresponding `ml` files are
+just the respective modules included.
+
+Here again, as for the previous example, we need to include some code. That is the
+extension of the `STM.ty` type. But also a `QCheck` generator for the `'a elt` type,
+as some function of the library take this type as argument.
+
+The generated code can be found in the respespective `varray*tests.ml` files.