Merge pull request #99 from inariksit/refman-updates

(refman) Add section about lists + links to my blog

1 files changed, 18 insertions, 1 deletions

diff --git a/doc/gf-refman.md b/doc/gf-refman.md
index 2a53041d9..503a5060c 100644
--- a/doc/gf-refman.md
+++ b/doc/gf-refman.md
@@ -1809,6 +1809,23 @@ As the last rule, subtyping is transitive:
 -   if *A* is a subtype of *B* and *B* is a subtype of *C*, then *A* is
     a subtype of *C*.
 
+### List categories
+
+[]{#lists}
+
+Since categories of lists of elements of another category are a common idiom, the following syntactic sugar is available:
+
+    cat [C] {n}
+
+abbreviates a set of three judgements:
+
+   cat ListC ;
+   fun BaseC : C -> ... -> C -> ListC ; --n C’s
+   fun ConsC : C -> ListC -> ListC
+
+The functions `BaseC` and `ConsC` are automatically generated in the abstract syntax, but their linearizations, as well as the linearization type of `ListC`, must be defined manually. The type expression `[C]` is in all contexts interchangeable with `ListC`.
+
+More information on lists in GF can be found [here](https://inariksit.github.io/gf/2021/02/22/lists.html).
 
 ### Tables and table types
 
@@ -2113,7 +2130,7 @@ of *x*, and the application thereby disappears.
 
 []{#reuse}
 
-*This section is valid for GF 3.0, which abandons the \"lock field\"*
+*This section is valid for GF 3.0, which abandons the \"[lock field](https://inariksit.github.io/gf/2018/05/25/subtyping-gf.html#lock-fields)\"*
 *discipline of GF 2.8.*
 
 As explained [here](#openabstract), abstract syntax modules can be