Merge branch 'master' into experimental

Author: MatthewDaggitt

CHANGELOG.md

@@ -1,7 +1,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 1.4-dev
+-- The Agda standard library, version 1.5-dev
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,
@@ -16,7 +16,8 @@ module README where
 -- Noam Zeilberger and other anonymous contributors.
 ------------------------------------------------------------------------
 
--- This version of the library has been tested using Agda 2.6.1.
+-- This version of the library has been tested using Agda 2.6.1 and
+-- 2.6.1.1.
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.

CHANGELOG/v1.4.md

@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Documentation describing some of the fixity choices
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- There is no actual code in here, just design note.
+
+module README.Design.Fixity where
+
+
+-- binary relations of all kinds are infix 4
+-- multiplication-like: infixl 7 _*_
+-- addition-like  infixl 6 _+_
+-- negation-like  infix  8 ¬_
+-- and-like  infixr 7 _∧_
+-- or-like  infixr 6 _∨_
+-- post-fix inverse  infix  8 _⁻¹
+-- bind infixl 1 _>>=_
+-- list concat-like infixr 5 _∷_
+-- ternary reasoning infix 1 _⊢_≈_
+-- composition infixr 9 _∘_
+-- application infixr -1 _$_ _$!_
+
+-- Reasoning:
+-- QED  infix  3 _∎
+-- stepping  infixr 2 _≡⟨⟩_ step-≡ step-≡˘
+-- begin  infix  1 begin_
+
+-- type formers:
+-- product-like infixr 2 _×_ _-×-_ _-,-_
+-- sum-like infixr 1 _⊎_

README.agda

@@ -1,5 +1,5 @@
 name:            lib
-version:         1.4-dev
+version:         1.5-dev
 cabal-version:   >= 1.10
 build-type:      Simple
 description:     Helper programs.

README/Design/Fixity.agda

@@ -1,19 +1,19 @@
 Installation instructions
 =========================
 
-Use version v1.3 of the standard library with Agda 2.6.1.
+Use version v1.4 of the standard library with Agda 2.6.1 and 2.6.1.1.
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where
    you would like to install the library.
 
-2. Download the tarball of v1.3 of the standard library. This can either be
+2. Download the tarball of v1.4 of the standard library. This can either be
    done manually by visiting the Github repository for the library, or via the
    command line as follows:
    ```
-   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.3.tar.gz
+   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.4.tar.gz
    ```
    Note that you can replace `wget` with other popular tools such as `curl` and that
-   you can replace `1.3` with any other version of the library you desire.
+   you can replace `1.4` with any other version of the library you desire.
 
 3. Extract the standard library from the tarball. Again this can either be
    done manually or via the command line as follows:
@@ -24,14 +24,14 @@ Use version v1.3 of the standard library with Agda 2.6.1.
 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
    the commands to install via cabal:
    ```
-   cd agda-stdlib-1.3
+   cd agda-stdlib-1.4
    cabal install
    ```
 
 5. Register the standard library with Agda's package system by adding
    the following line to `$HOME/.agda/libraries`:
    ```
-   $HERE/agda-stdlib-1.3/standard-library.agda-lib
+   $HERE/agda-stdlib-1.4/standard-library.agda-lib
    ```
 
 Now, the standard library is ready to be used either:

lib.cabal

@@ -26,6 +26,10 @@ procedure should be followed:
     cd agda
     make fast-forward-std-lib
 
+* Build the latest version of Agda
+
+    make quicker-install-bin
+
 * Run the tests involving the library:
 
     make test

notes/installation-guide.md

@@ -151,13 +151,13 @@ fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
 fromℕ-def zero    = refl
 fromℕ-def (suc n) = cong suc (fromℕ-def n)
 
-fromℕ<-irrelevant : ∀ m n {o} → m ≡ n →
-                    (m<o : m ℕ.< o) →
-                    (n<o : n ℕ.< o) →
-                    fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-irrelevant 0 0 r (s≤s z≤n) (s≤s z≤n) = refl
-fromℕ<-irrelevant (suc _) (suc _) r (s≤s (s≤s p)) (s≤s (s≤s q))
-  = cong suc (fromℕ<-irrelevant _ _ (ℕₚ.suc-injective r) (s≤s p) (s≤s q))
+fromℕ<-cong : ∀ m n {o} → m ≡ n →
+              (m<o : m ℕ.< o) →
+              (n<o : n ℕ.< o) →
+              fromℕ< m<o ≡ fromℕ< n<o
+fromℕ<-cong 0       0       r (s≤s z≤n)     (s≤s z≤n)     = refl
+fromℕ<-cong (suc _) (suc _) r (s≤s (s≤s p)) (s≤s (s≤s q))
+  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) (s≤s p) (s≤s q))
 
 fromℕ<-injective : ∀ m n {o} →
                    (m<o : m ℕ.< o) →

notes/release-guide.txt

@@ -170,6 +170,8 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
 -- Finds the context and remaining graph corresponding to a given node
 -- index.
 
+  infix 4 _[_]
+
   _[_] : ∀ {n} → Graph N E n → (i : Fin n) → Graph N E (suc (n - suc i))
   (c & g) [ zero ]  = c & g
   (c & g) [ suc i ] = g [ i ]

src/Data/Fin/Properties.agda

@@ -127,6 +127,8 @@ module ∣-Reasoning where
 ------------------------------------------------------------------------
 -- Other properties of _∣_
 
+infix 4 _∣?_
+
 _∣?_ : Decidable _∣_
 k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣)