7 files changed, 94 insertions, 24 deletions
diff --git a/README/AVL.agda b/README/AVL.agda
index bc96d06..8a2fdea 100644
--- a/README/AVL.agda
+++ b/README/AVL.agda
@@ -21,7 +21,8 @@ open import Data.Nat.Properties using (<-isStrictTotalOrder)
 open import Data.String using (String)
 open import Data.Vec using (Vec; _∷_; [])
 
-open Data.AVL (Vec String) (<-isStrictTotalOrder)
+open Data.AVL <-isStrictTotalOrder renaming (Tree to Tree')
+Tree = Tree' (Vec String)
 
 ------------------------------------------------------------------------
 -- Construction of trees
@@ -58,6 +59,7 @@ t₃ = delete 2 t₂
 open import Data.List using (_∷_; [])
 open import Data.Product as Prod using (_,_; _,′_)
 
+t₄ : Tree
 t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])
 
 ------------------------------------------------------------------------
diff --git a/README/Case.agda b/README/Case.agda
index e42f55a..229acf8 100644
--- a/README/Case.agda
+++ b/README/Case.agda
@@ -22,8 +22,8 @@ pred n = case n of λ
   ; (suc n) → n
   }
 
-from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x
-from-just x = case x return From-just _ of λ
+from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x
+from-just x = case x return From-just of λ
   { (just x) → x
   ; nothing  → _
   }
diff --git a/README/Container/FreeMonad.agda b/README/Container/FreeMonad.agda
index c7b3eec..b0b7654 100644
--- a/README/Container/FreeMonad.agda
+++ b/README/Container/FreeMonad.agda
@@ -24,19 +24,19 @@ open import Relation.Binary.PropositionalEquality
 
 -- The signature of state and its (generic) operations.
 
-State : Set → Container _
+State : Set → Container _ _
 State S = ⊤ ⟶ S ⊎ S ⟶ ⊤
   where
-  _⟶_ : Set → Set → Container _
+  _⟶_ : Set → Set → Container _ _
   I ⟶ O = I ▷ λ _ → O
 
 get : ∀ {S} → State S ⋆ S
-get = do (inj₁ _ , return)
+get = inn (inj₁ _ , return)
   where
   open RawMonad rawMonad
 
 put : ∀ {S} → S → State S ⋆ ⊤
-put s = do (inj₂ s , return)
+put s = inn (inj₂ s , return)
   where
   open RawMonad rawMonad
 
@@ -50,10 +50,10 @@ prog =
   where
   open RawMonad rawMonad
 
-runState : ∀ {S X} → State S ⋆ X → (S → X ⟨×⟩ S)
-runState (sup (inj₁ x) _)        = λ s → x , s
-runState (sup (inj₂ (inj₁ _)) k) = λ s → runState (k s) s
-runState (sup (inj₂ (inj₂ s)) k) = λ _ → runState (k _) s
+runState : {S X : Set} → State S ⋆ X → (S → X ⟨×⟩ S)
+runState (sup (inj₁ x , _))        = λ s → x , s
+runState (sup (inj₂ (inj₁ _) , k)) = λ s → runState (k s) s
+runState (sup (inj₂ (inj₂ s) , k)) = λ _ → runState (k _) s
 
 test : runState prog 0 ≡ (true , 1)
 test = refl
diff --git a/README/Function/Reasoning.agda b/README/Function/Reasoning.agda
new file mode 100644
index 0000000..b28f27d
--- /dev/null
+++ b/README/Function/Reasoning.agda
@@ -0,0 +1,67 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some examples showing how the Function.Reasoning module
+-- can be used to perform "functional reasoning" similar to what is being
+-- described in: https://stackoverflow.com/q/22676703/3168666
+------------------------------------------------------------------------
+
+module README.Function.Reasoning where
+
+-- Function.Reasoning exports a flipped application (_|>_) combinator
+-- as well as a type annotation (_∶_) combinator.
+
+open import Function.Reasoning
+
+------------------------------------------------------------------------
+-- A simple example
+
+module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where
+
+-- Using the combinators we can, starting from a value, chain various
+-- functions whilst tracking the types of the intermediate results.
+
+  A→C : A → C
+  A→C a =
+       a    ∶ A
+    |> A→B  ∶ B
+    |> B→C  ∶ C
+
+------------------------------------------------------------------------
+-- A more concrete example
+
+open import Data.Nat
+open import Data.List.Base
+open import Data.Char.Base
+open import Data.String using (String; toList; fromList)
+open import Data.String.Unsafe using (_==_)
+open import Function
+open import Data.Bool
+open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
+open import Agda.Builtin.Equality
+
+-- This can give us for instance this decomposition of a function
+-- collecting all of the substrings of the input which happen to be
+-- palindromes:
+
+subpalindromes : String → List String
+subpalindromes str = let Chars = List Char in
+     str                                   ∶ String
+  -- first generate the substrings
+  |> toList                                ∶ Chars
+  |> inits                                 ∶ List Chars
+  |> concatMap tails                       ∶ List Chars
+  -- then only keeps the ones which are not singletons
+  |> filter (λ cs → 2 ≤? length cs)        ∶ List Chars
+  -- only keep the ones that are palindromes
+  |> map < fromList , fromList ∘ reverse > ∶ List (String × String)
+  |> boolFilter (uncurry _==_)             ∶ List (String × String)
+  |> map proj₁                             ∶ List String
+
+-- Test cases
+
+_ : subpalindromes "doctoresreverse" ≡ "eve" ∷ "rever" ∷ "srevers" ∷ "esreverse" ∷ []
+_ = refl
+
+_ : subpalindromes "elle-meme" ≡ "ll" ∷ "elle" ∷ "mem" ∷ "eme" ∷ []
+_ = refl
diff --git a/README/Integer.agda b/README/Integer.agda
index c6e3469..08a1ade 100644
--- a/README/Integer.agda
+++ b/README/Integer.agda
@@ -40,13 +40,10 @@ ex₄ = P.refl
 -- integers. Algebra defines what a commutative ring is, among other
 -- things.
 
-open import Algebra
-import Data.Integer.Properties as Integer
-private
-  module CR = CommutativeRing Integer.commutativeRing
+import Data.Integer.Properties as ℤₚ
 
 ex₅ : ∀ i j → i * j ≡ j * i
-ex₅ i j = CR.*-comm i j
+ex₅ i j = ℤₚ.*-comm i j
 
 -- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
 -- provides some combinators for equational reasoning.
@@ -56,15 +53,17 @@ open import Data.Product
 
 ex₆ : ∀ i j → i * (j + + 0) ≡ j * i
 ex₆ i j = begin
-  i * (j + + 0)  ≡⟨ P.cong (_*_ i) (proj₂ CR.+-identity j) ⟩
-  i * j          ≡⟨ CR.*-comm i j ⟩
+  i * (j + + 0)  ≡⟨ P.cong (i *_) (ℤₚ.+-identityʳ j) ⟩
+  i * j          ≡⟨ ℤₚ.*-comm i j ⟩
   j * i          ∎
 
--- The module RingSolver in Data.Integer.Properties contains a solver
+-- The module RingSolver in Data.Integer.Solver contains a solver
 -- for integer equalities involving variables, constants, _+_, _*_, -_
 -- and _-_.
 
+open import Data.Integer.Solver using (module +-*-Solver)
+open +-*-Solver
+
 ex₇ : ∀ i j → i * - j - j * i ≡ - + 2 * i * j
 ex₇ = solve 2 (λ i j → i :* :- j :- j :* i  :=  :- con (+ 2) :* i :* j)
               P.refl
-  where open Integer.RingSolver
diff --git a/README/Nat.agda b/README/Nat.agda
index b6afd17..c5782cf 100644
--- a/README/Nat.agda
+++ b/README/Nat.agda
@@ -42,11 +42,12 @@ ex₄ m n = begin
   m * n        ≡⟨ Nat.*-comm m n ⟩
   n * m        ∎
 
--- The module SemiringSolver in Data.Nat.Properties contains a solver
+-- The module SemiringSolver in Data.Nat.Solver contains a solver
 -- for natural number equalities involving variables, constants, _+_
 -- and _*_.
 
-open Nat.SemiringSolver
+open import Data.Nat.Solver using (module +-*-Solver)
+open +-*-Solver
 
 ex₅ : ∀ m n → m * (n + 0) ≡ n * m
 ex₅ = solve 2 (λ m n → m :* (n :+ con 0)  :=  n :* m) refl
diff --git a/README/Record.agda b/README/Record.agda
index 4e8f06e..7994cb2 100644
--- a/README/Record.agda
+++ b/README/Record.agda
@@ -11,6 +11,7 @@ module README.Record where
 
 open import Data.Product
 open import Data.String
+open import Data.String.Unsafe
 open import Function using (flip)
 open import Level
 import Record
@@ -25,8 +26,8 @@ open Record String _≟_
 PER : Signature _
 PER = ∅ , "S"     ∶ (λ _ → Set)
         , "R"     ∶ (λ r → r · "S" → r · "S" → Set)
-        , "sym"   ∶ (λ r → Lift (Symmetric (r · "R")))
-        , "trans" ∶ (λ r → Lift (Transitive (r · "R")))
+        , "sym"   ∶ (λ r → Lift _ (Symmetric (r · "R")))
+        , "trans" ∶ (λ r → Lift _ (Transitive (r · "R")))
 
 -- Given a PER the converse relation is also a PER.