improve documentation

docs/org/SUMMARY.org

@@ -25,13 +25,13 @@
 * Reference
 - [[./reference/stdlib.md][Standard library]]
 - [[./reference/language/README.md][Language reference]]
-  - [[./reference/language/comments.md][Comments]]
-  - [[./reference/language/axiom.md][Axiom]]
-  - [[./reference/language/compileblocks.md][Compile block]]
-  - [[./reference/language/modules.md][Module]]
+  - [[./reference/language/functions.md][Functions]]
   - [[./reference/language/datatypes.md][Data types]]
-  - [[./reference/languages/functions.md][Function]]
-  - [[./reference/language/foreign.md][Foreign block]]
+  - [[./reference/language/modules.md][Modules]]
+  - [[./reference/language/comments.md][Comments]]
+  - [[./reference/language/axioms.md][Axioms]]
+  - [[./reference/language/compileblocks.md][Compile blocks]]
+  - [[./reference/language/foreign.md][Foreign blocks]]
 - [[./reference/examples.md][Example programs]]
 - [[./reference/benchmarks.md][Benchmarks]]
 - [[./reference/tooling/README.md][Tooling]]

docs/org/howto/installing.org

@@ -9,7 +9,7 @@ If you want to compile to WebAssembly, you also need:
 - [[https://lld.llvm.org][wasm-ld]] - the LLVM linker for WASM (NB: On Linux you may need to install the
   =lld= package; on macOS this is installed as part of =llvm=).
 
-See [[./installing.md#installing-dependencies][below]] for instruction on how to install the dependencies.
+See [[./installing.md#installing-dependencies][below]] for instructions on how to install the dependencies.
 
 * Installing Juvix
 
@@ -30,7 +30,7 @@ brew install juvix
 #+end_src
 
 
-Helpful information on the shell can also be obtained by running:
+Helpful information can also be obtained by running:
 
 #+begin_src shell
 brew info juvix
@@ -40,10 +40,10 @@ brew info juvix
 
 A Juvix compiler binary executable for Linux x86_64 is available on the [[https://github.com/anoma/juvix/releases/latest][Juvix release page]].
 
-To install this executable, downlaod and unzip the linked file and add move it
+To install this executable, downlaod and unzip the linked file and move it
 to a directory on your shell's =PATH=.
 
-For example if =~/.local/bin= is on your shell's =PATH= you can install Juvix as
+For example if =~/.local/bin= is on your shell's =PATH=, you can install Juvix as
 follows:
 
 #+begin_src shell
@@ -68,8 +68,8 @@ The C compiler and linker paths can be specified as options to the =make install
 make install CC=path/to/clang LIBTOOL=path/to/llvm-ar
 #+end_src
 
-On MacOS you can alternatively run the following command for Homebrew. The flag
-=--HEAD= used below is optional, use it to build the latest version of Juvix in
+On MacOS, you can alternatively run the following command for Homebrew. The flag
+=--HEAD= used below is optional -- use it to build the latest version of Juvix in
 the =main= branch on Github.
 
 #+begin_src shell
@@ -80,7 +80,7 @@ brew install --build-from-source --HEAD juvix --verbose
 
 We recommend to use the =stack= build tool with this project.
 
-If you would prefer to use the =cabal= build tool instead then you must generate
+If you prefer the =cabal= build tool instead, then you need to generate
 the =juvix.cabal= file using [[https://github.com/sol/hpack][hpack]] before running =cabal build=.
 
 You also need to compile the runtime first:

docs/org/quick-start.org

@@ -8,7 +8,7 @@
 
 To install Juvix, follow the instruction in the  [[./howto/installing.md][Installation How-to]].
 
-After installation, run =juvix --help= to see the list of commands available.
+After installation, run =juvix --help= to see the list of commands.
 
 Run Juvix doctor to check your system setup:
 

docs/org/reference/language/README.org

@@ -1,7 +1,7 @@
+  - [[./functions.md][Functions]]
+  - [[./datatypes.md][Data types]]
+  - [[./modules.md][Modules]]
   - [[./comments.md][Comments]]
-  - [[./axiom.md][Axiom]]
-  - [[./functions.md][Function]]
-  - [[./modules.md][Module System]]
-  - [[./datatypes.md][Inductive data types]]
+  - [[./axioms.md][Axioms]]
   - [[./compileblocks.md][Compile blocks]]
   - [[./foreign.md][Foreign blocks]]

docs/org/reference/language/datatypes.org

@@ -1,31 +1,28 @@
-* Inductive data types
+* Data types
 
-The =inductive= keyword is reserved for declaring inductive data types. An
-inductive type declaration requires a unique name for its type and a non-empty
-list of constructor declarations, functions for building the terms of the
-inductive data type. Constructors can be used as normal identifiers and also in
-patterns. As shown later, one can also provide type parameters to widen the
-family of inductive types one can define in Juvix.
+A data type declaration consists of:
+- the =type= keyword,
+- a unique name for the type,
+- the =:== symbol,
+- a non-empty list of constructor declarations -- functions for building the elements of the data type.
 
-The simplest inductive type is the =Unit= type with one constructor called =unit=.
+The simplest data type is the =Unit= type with one constructor called =unit=.
 
 #+begin_example
 type Unit := unit : Unit;
 #+end_example
 
-In the following example, we declare the inductive type =Nat=, the unary
-representation of natural numbers. This type comes with two data constructors,
-namely =zero= and =suc=. A term of the type =Nat= is the number one, represented
-by =suc zero= or the number two represented by =suc (suc zero)=, etc.
+In the following example, we declare the type =Nat= -- the unary
+representation of natural numbers. This type comes with two constructors: =zero= and =suc=. Example elements of type =Nat= are the number one represented
+by =suc zero=, the number two represented by =suc (suc zero)=, etc.
 
 #+begin_example
 type Nat :=
     zero : Nat
   | suc : Nat -> Nat;
 #+end_example
 
-The way to use inductive types is by declaring functions by pattern matching.
-Let us define, for example, the function for adding two natural numbers.
+Constructors can be used like normal functions or in patterns when defining functions by pattern matching. For example, here is a function adding two natural numbers:
 
 #+begin_src text
 inifl 6 +;
@@ -34,12 +31,9 @@ inifl 6 +;
 + (suc a) b := suc (a + b);
 #+end_src
 
-As mentioned earlier, an inductive type may have type parameters. The canonical
-example is the polymorphic type =List=. The type =List= is the inductive type that
-considers the type of the elements in the list as a parameter. A constructor to
-build the empty list, that is the base case, and another constructor to enlarge
-the list, we usually called it =cons=. One possible definition for this type is
-the following type taken from the Juvix standard library:
+A data type may have type parameters. A data type with a type
+parameter =A= is called /polymorphic in/ =A=. A canonical example is
+the type =List= polymorphic in the type of list elements.
 
 #+begin_example
 infixr 5 ::;
@@ -52,5 +46,5 @@ elem _ _ nil := false;
 elem eq s (x :: xs) := eq s x || elem eq s xs;
 #+end_example
 
-To see more examples of inductive types and how to use them, please check out
-[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]]
+For more examples of inductive types and how to use them, see
+[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]].

docs/org/reference/language/functions.org

@@ -1,9 +1,8 @@
 * Function declaration
 
-A function declaration is a type signature /and/ a group of definitions called
-/function clauses/.
+A function declaration consists of a type signature and a group of /function clauses/.
 
-In the following example we define a function called =multiplyByTwo=. The first
+In the following example, we define a function =multiplyByTwo=. The first
 line =multiplyByTwo : Nat -> Nat;= is the type signature and the second line
 ~multiplyByTwo n := 2 * n;~ is a function clause.
 
@@ -27,13 +26,13 @@ neg true := false;
 neg false := true;
 #+end_example
 
-When =neg= is called with =true= the first clause is used and the function
-returns =false=. Similarly, when =neg= is called with =false= the second clause
+When =neg= is called with =true=, the first clause is used and the function
+returns =false=. Similarly, when =neg= is called with =false=, the second clause
 is used and the function returns =true=.
 
 ** Mutually recursive functions
 
-Function declarations can depend on others recursively. In the following example we define a function that checks if a number is =even= by calling a function that checks if a number is =odd=.
+Function declarations can depend on each other recursively. In the following example, we define a function that checks if a number is =even= by calling a function that checks if a number is =odd=.
 
 #+begin_example
 open import Stdlib.Prelude;