docs: various minor updates

docs/quickstart.mld

@@ -4,21 +4,21 @@ This tutorial is for an implementer (you!) to integrate this library into your t
 
 {1 Introduction}
 
-Following {{: https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf} Conor McBride’s crude but effective stratification} and {{: https://doi.org/10.1145/3571250} our algebraic reformulation}, a universe level in this library is represented as a pair of a variable together with some {i displacement}. For example, a universe level might be [x + 10], meaning the variable level [x] shifted (bumped) by 10 levels. The shifting of 10 levels is the displacement. For the same variable [x], the level [x + n] is larger than [x + m] if [n] is larger than [m], while levels [x + n] and [y + m] are in general incomparable for different variables [x] and [y]. Substituting [x + n1] for [y] in [y + n2] results in the level [x + (n1 + n2)].
+Following {{: https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf} Conor McBride’s crude but effective stratification} and {{: https://doi.org/10.1145/3571250} our algebraic reformulation}, a universe level in this library is represented as a pair of a variable together with some {e displacement}. For example, a universe level might be [x + 10], meaning the variable level [x] shifted (bumped) by 10 levels. The shifting of 10 levels is the displacement. For the same variable [x], the level [x + n] is larger than [x + m] if [n] is larger than [m], while levels [x + n] and [y + m] are in general incomparable for different variables [x] and [y]. Substituting [x + n1] for [y] in [y + n2] results in the level [x + (n1 + n2)].
 
-While this scheme (with only a variable and some displacement) looks limited, we proved that it is in a sense {e universal} if you allow all mathematically possible displacements beyond natural numbers. We also call the minimum algebra of displacements that would make the scheme work a {i displacement algebra}. See our {{: https://doi.org/10.1145/3571250} POPL paper} for more details.
+While this scheme (with only a variable and some displacement) looks limited, we proved that it is in a sense {e universal} if you allow all mathematically possible displacements beyond natural numbers. We also call the minimum algebra of displacements that would make the scheme work a {e displacement algebra}. See our {{: https://doi.org/10.1145/3571250} POPL paper} for more details.
 
 This library implements several displacement algebras you could choose from, along with a uniform interface to construct and compare universe levels.
 
 {1 Choose Your Displacements}
 
-The first step is to choose your favorite {i displacements}. We will use {!module:Mugen.Shift.Int} (integers) as the starting point, and it is easy to switch to another displacement algebra later. Other displacements are under {!module:Mugen.Shift} and {!module:Mugen.ShiftWithJoin}.
+The first step is to choose your favorite {e displacements}. We will use {!module:Mugen.Shift.Int} (integers) as the starting point, and it is easy to switch to another displacement algebra later. Other displacements are under {!module:Mugen.Shift} and {!module:Mugen.ShiftWithJoin}.
 
 {1 Free Level Expressions}
 
-{i Free} level expressions are expressions freely generated by only variables and shifting operators. In contrast, we will have a different kind of level expressions embedded in your datatype holding terms or types. The free level expressions are the only ones that can be compared against each other, while the embedded ones must be converted to free ones before comparing them. More on this later.
+{e Free} level expressions are expressions freely generated by only variables and shifting operators. In contrast, we will have a different kind of level expressions embedded in your datatype holding terms or types. The free level expressions are the only ones that can be compared against each other; the embedded ones must be converted to free ones for comparison. More on this point later.
 
-Save the following file as [ULvl.ml] for free level expressions, assuming that you are using integers to represent variables.
+Save the following content as the file [ULvl.ml] for free level expressions, assuming that you are using integers to represent variables.
 
 {[
 module Param =

example/Domain.ml

@@ -25,7 +25,7 @@ and endo_to_ulvl : ulvl -> ULvl.t =
   | M.Shifted (l, s) -> ULvl.shifted (to_ulvl l) s
   | M.Top -> ULvl.top
 
-(** Smart builders for universe levels *)
+(** Smart constructors for universe levels *)
 include
   Mugen.Builder.Endo.Make
     (struct

example/ULvl.ml

@@ -19,7 +19,7 @@ type shift = Shift.t
 (** An alias to the type of free level expressions *)
 type t = (shift, int) Mugen.Syntax.free
 
-(** Smart builders for free level expressions *)
+(** Smart constructors for free level expressions *)
 include Mugen.Builder.Free.Make (Param)
 
 (** Comparators for free level expressions *)

src/Mugen.mli

@@ -8,15 +8,15 @@ module ShiftWithJoin : module type of ShiftWithJoin
 
 (** {1 Syntax of Level Expressions} *)
 
-(** Syntax of universe level expressions *)
+(** Definitions of level expressions *)
 module Syntax : module type of Syntax
 
-(** Smart builders for universe level expressions *)
+(** Smart constructors for level expressions *)
 module Builder : module type of Builder
 
 (** {1 Comparators of Level Expressions} *)
 
-(** Semantic operations for universe levels with displacements *)
+(** Semantic comparators for free level expressions *)
 module Theory : module type of Theory
 
 (**/**)