Improve pointers to README files and rename README.Dec (#975)

Author: MatthewDaggitt

README.agda

@@ -262,6 +262,10 @@ import IO
 -- More documentation
 ------------------------------------------------------------------------
 
+-- Examples of how decidability is handled in the library.
+
+import README.Decidability
+
 -- Some examples showing how the case expression can be used.
 
 import README.Case

README/Dec.agda renamed to README/Decidability.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module README.Dec where
+module README.Decidability where
 
 -- Reflects and Dec are defined in Relation.Nullary, and operations on them can
 -- be found in Relation.Nullary.Reflects and Relation.Nullary.Decidable.

src/Data/AVL.agda

@@ -9,6 +9,8 @@
 -- The search tree invariant is specified using the technique
 -- described by Conor McBride in his talk "Pivotal pragmatism".
 
+-- See README.Data.AVL for examples of how to use AVL trees.
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (StrictTotalOrder)

src/Data/Integer.agda

@@ -4,6 +4,9 @@
 -- Integers
 ------------------------------------------------------------------------
 
+-- See README.Data.Integer for examples of how to use and reason about
+-- integers.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Integer where

src/Data/Integer/Base.agda

@@ -4,6 +4,9 @@
 -- Integers, basic types and operations
 ------------------------------------------------------------------------
 
+-- See README.Data.Integer for examples of how to use and reason about
+-- integers.
+
 {-# OPTIONS --without-K --safe #-}
 
 -- Disabled to prevent warnings from deprecated names

src/Data/List.agda

@@ -4,6 +4,9 @@
 -- Lists
 ------------------------------------------------------------------------
 
+-- See README.Data.List for examples of how to use and reason about
+-- lists.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.List where

src/Data/List/Base.agda

@@ -4,6 +4,9 @@
 -- Lists, basic types and operations
 ------------------------------------------------------------------------
 
+-- See README.Data.List for examples of how to use and reason about
+-- lists.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.List.Base where

src/Data/List/Fresh.agda

@@ -6,6 +6,9 @@
 -- Lambda-Calculus with Explicit Substitutions"
 ------------------------------------------------------------------------
 
+-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
+-- examples of how to use fresh lists.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.List.Fresh where

src/Data/Nat.agda

@@ -4,6 +4,9 @@
 -- Natural numbers
 ------------------------------------------------------------------------
 
+-- See README.Data.Nat for examples of how to use and reason about
+-- naturals.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Nat where

src/Data/Nat/Base.agda

@@ -4,6 +4,9 @@
 -- Natural numbers, basic types and operations
 ------------------------------------------------------------------------
 
+-- See README.Data.Nat for examples of how to use and reason about
+-- naturals.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Nat.Base where