Add missing Func record to Function.Bundles (#1353)

Author: MatthewDaggitt

CHANGELOG.md

@@ -285,3 +285,22 @@ Other minor additions
   ```
 
 * Added infix declarations to `Data.Product.∃-syntax` and `Data.Product.∄-syntax`.
+
+* Added new definitions to `Function.Bundles`:
+  ```agda
+  record Func : Set _
+  _⟶_ : Set a → Set b → Set _
+  mk⟶ : (A → B) → A ⟶ B
+  ```
+
+* Added new proofs to `Function.Construct.Composition`:
+  ```agda
+  function : Func R S → Func S T → Func R T
+  _∘-⟶_    : (A ⟶ B) → (B ⟶ C) → (A ⟶ C)
+  ```
+
+* Added new proofs to `Function.Construct.Identity`:
+  ```agda
+  function : Func S S
+  id-⟶     : A ⟶ A
+  ```

README/Case.agda

@@ -15,7 +15,7 @@ open import Data.Nat   hiding (pred)
 open import Data.List
 open import Data.Sum
 open import Data.Product
-open import Function using (case_of_; case_return_of_)
+open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality

README/Data/Nat/Induction.agda

@@ -10,7 +10,7 @@ module README.Data.Nat.Induction where
 open import Data.Nat
 open import Data.Nat.Induction
 open import Data.Product using (_,_)
-open import Function using (_∘_)
+open import Function.Base using (_∘_)
 open import Induction.WellFounded
 open import Relation.Binary.PropositionalEquality
 

README/Data/Record.agda

@@ -13,7 +13,7 @@ module README.Data.Record where
 
 open import Data.Product
 open import Data.String
-open import Function using (flip)
+open import Function.Base using (flip)
 open import Level
 open import Relation.Binary
 

README/Data/Tree/AVL.agda

@@ -106,7 +106,7 @@ q₅′ = refl
 -- Partitioning a tree into the smallest element plus the rest, or the
 -- largest element plus the rest.
 
-open import Function using (id)
+open import Function.Base using (id)
 
 v₆ : headTail t₀ ≡ nothing
 v₆ = refl

README/Data/Trie/NonDependent.agda

@@ -60,7 +60,7 @@ open import Data.Product     as Prod
 open import Data.String      as String using (String)
 open import Data.These       as These
 
-open import Function using (case_of_; _$_; _∘′_; id; _on_)
+open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
 open import Relation.Binary using (Rel)
 open import Relation.Nullary.Negation using (¬?)

notes/style-guide.md

@@ -31,6 +31,51 @@ automate most of this.
   should always go at the end of the line rather than the beginning of the
   next line.
 
+#### Empty lines
+
+* All module headers and standard term definitions should have a single
+  empty line after them.
+
+* There should be _two_ empty lines between adjacent record or module definitions
+  in order to better distinguish the end of the record or module, as they will
+  already be using single empty lines between internal definitions.
+
+* For example:
+  ```agda
+  module Test1 where
+
+    def1 : ...
+    def1 = ...
+
+    def2 : ...
+    def2 = ...
+
+
+  module Test2 where
+
+    record Record1 : Set where
+      field
+        field1 : ...
+
+      aux1 : ...
+      aux1 = ...
+
+      aux2 : ...
+      aux2 = ...
+
+
+   record Record2 : Set where
+     field
+       field2 : ...
+
+
+   record1 : Record1
+   record1 = { field1 = ... }
+
+   record2 : Record2
+   record2 = { field2 = ... }
+  ```
+
 #### Modules
 
 * As a rule of thumb there should only be one named module per file. Anonymous

src/Algebra/Construct/NaturalChoice/Min.agda

@@ -16,7 +16,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Data.Sum.Base using (inj₁; inj₂; [_,_])
 open import Data.Product using (_,_)
-open import Function using (id)
+open import Function.Base using (id)
 
 open TotalOrder totalOrder renaming (Carrier to A)
 open import Algebra.Definitions _≈_

src/Algebra/Operations/CommutativeMonoid.agda

@@ -13,7 +13,7 @@ open import Algebra
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.Fin.Base using (Fin; zero)
 open import Data.Table.Base as Table using (Table)
-open import Function using (_∘_)
+open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid

src/Algebra/Operations/Semiring.agda

@@ -19,7 +19,7 @@ import Algebra.Operations.CommutativeMonoid as MonoidOperations
 open import Data.Nat.Base
   using (zero; suc; ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
 open import Data.Product using (module Σ)
-open import Function using (_$_)
+open import Function.Base using (_$_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)