[ fix ] We can't turn non-fatal error warnings anymore

Author: gallais

README/Data/List/Relation/Binary/Equality.agda

@@ -4,7 +4,7 @@
 -- Documentation for pointwise equality over `List`s
 ------------------------------------------------------------------------
 
-{-# OPTIONS --warning noMissingDefinitions #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 
 module README.Data.List.Relation.Binary.Equality where
 
@@ -37,6 +37,7 @@ lem₁ = refl
 -- equality of two lists of the type `List (ℕ → ℕ)`:
 
 lem₂ : (λ x → 2 * x + 2) ∷ [] ≡ (λ x → 2 * (x + 1)) ∷ []
+lem₂ = {!!}
 
 -- In such a case it is impossible to prove the two lists equal with
 -- refl as the two functions are not propositionally equal. In the
@@ -56,6 +57,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise)
 
 lem₃ : Pointwise _≗_ ((λ x → x + 1) ∷ []) ((λ x → x + 2 ∸ 1) ∷ [])
+lem₃ = {!!}
 
 -- the library provides some nicer wrappers and infix notation in the
 -- folder "Data.List.Relation.Binary.Equality".

README/Design/Hierarchies.agda

@@ -4,7 +4,7 @@
 -- An explanation about how mathematical hierarchies are laid out.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --warning noMissingDefinitions #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 
 module README.Design.Hierarchies where
 
@@ -261,9 +261,11 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 -- one to translate between left and right identities.
 
 total⇒refl : ∀ {_∼_ : Rel A ℓ} → Total _∼_ → Reflexive _∼_
+total⇒refl = {!!}
 
 idˡ+comm⇒idʳ : ∀ {_≈_ : Rel A ℓ} {e _∙_} → Commutative _≈_ _∙_ →
                LeftIdentity _≈_ e _∙_ →  RightIdentity _≈_ e _∙_
+idˡ+comm⇒idʳ = {!!}
 
 ------------------------------------------------------------------------
 -- X.Construct