From 2d379fb250553c6cd23ba54d5fb652e973e1ef98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 31 Dec 2021 19:24:23 +0100
Subject: [PATCH] Documentation comments.

---
 feat/Enum.mli  | 6 ++++++
 feat/IFSeq.mli | 8 ++++++++
 feat/Num.mli   | 2 ++
 3 files changed, 16 insertions(+)

diff --git a/feat/Enum.mli b/feat/Enum.mli
index ec0de7c..58caf98 100644
--- a/feat/Enum.mli
+++ b/feat/Enum.mli
@@ -8,4 +8,10 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module offers a concrete data type ['a enum] of {b enumerations} of
+   elements of type ['a]. Suppose that every element of type ['a] is
+   implicitly assigned a certain size. Then, an enumeration is a function of
+   an integer [s] to the (implicit, finite) sequence of all elements whose
+   size is [s]. *)
+
 include FeatCore.EnumSig.ENUM with module IFSeq = IFSeq
diff --git a/feat/IFSeq.mli b/feat/IFSeq.mli
index 0ae02c5..570d6db 100644
--- a/feat/IFSeq.mli
+++ b/feat/IFSeq.mli
@@ -8,4 +8,12 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module provides an abstract data type of {b implicit, finite
+   sequences}. An implicit sequence is not explicitly represented in memory
+   as an actual sequence of elements: instead, it is {e described} by a data
+   structure which contains enough information to produce an arbitrary
+   element upon request. This design decision imposes some constraints on
+   the operations that can be efficiently supported: for instance, [filter]
+   is not supported. *)
+
 include FeatCore.IFSeqSig.IFSEQ_EXTENDED with type index = Num.t
diff --git a/feat/Num.mli b/feat/Num.mli
index 4c771fc..2f8e456 100644
--- a/feat/Num.mli
+++ b/feat/Num.mli
@@ -8,6 +8,8 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module implements a small set of operations on big integers. *)
+
 (* This module satisfies the signature [BigIntSig.EXTENDED],
    instantiated with unbounded integers from [zarith]. *)
 include FeatCore.BigIntSig.EXTENDED with type t = Z.t
-- 
GitLab