[ fix #547 ] Add --safe flags to all safe modules (#549)

agda · Dec 7, 2018 · 64c9035 · 64c9035
1 parent d7d3831
commit 64c9035
Show file tree

Hide file tree

Showing 392 changed files with 393 additions and 391 deletions.
diff --git a/src/Algebra.agda b/src/Algebra.agda
@@ -5,7 +5,7 @@
 -- (packed in records together with sets, operations, etc.)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra where
 

diff --git a/src/Algebra/FunctionProperties.agda b/src/Algebra/FunctionProperties.agda
@@ -4,7 +4,7 @@
 -- Properties of functions, such as associativity and commutativity
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Level
 open import Relation.Binary

diff --git a/src/Algebra/FunctionProperties/Consequences.agda b/src/Algebra/FunctionProperties/Consequences.agda
@@ -5,7 +5,7 @@
 -- commutativity
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
 

diff --git a/src/Algebra/FunctionProperties/Consequences/Propositional.agda b/src/Algebra/FunctionProperties/Consequences/Propositional.agda
@@ -5,7 +5,7 @@
 -- commutativity (specialised to propositional equality)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.FunctionProperties.Consequences.Propositional
        {a} {A : Set a} where

diff --git a/src/Algebra/FunctionProperties/Core.agda b/src/Algebra/FunctionProperties/Core.agda
@@ -9,7 +9,7 @@
 -- Algebra.FunctionProperties is a parameterised module, and some of
 -- the parameters are irrelevant for these definitions.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.FunctionProperties.Core where
 

diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda
@@ -4,7 +4,7 @@
 -- Morphisms between algebraic structures
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Morphism where
 

diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda
@@ -5,7 +5,7 @@
 -- exponentiation)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda
@@ -5,7 +5,7 @@
 -- exponentiation)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Properties/BooleanAlgebra/Expression.agda
@@ -4,7 +4,7 @@
 -- Boolean algebra expressions
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda
@@ -4,7 +4,7 @@
 -- Some derivable properties
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -6,7 +6,7 @@
 -- Adapted from Algebra.Monoid-solver
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Solver/CommutativeMonoid/Example.agda b/src/Algebra/Solver/CommutativeMonoid/Example.agda
@@ -4,7 +4,7 @@
 -- An example of how Algebra.CommutativeMonoidSolver can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Solver.CommutativeMonoid.Example where
 

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -6,7 +6,7 @@
 -- Adapted from Algebra.Monoid-solver
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda
@@ -5,7 +5,7 @@
 -- used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Solver.IdempotentCommutativeMonoid.Example where
 

diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
@@ -4,7 +4,7 @@
 -- Solver for monoid equalities
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
@@ -15,7 +15,7 @@
 -- more equalities it returns, the more expressions the ring solver can
 -- solve.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 open import Algebra.Solver.Ring.AlmostCommutativeRing

diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
@@ -5,7 +5,7 @@
 -- commutative rings), used by the ring solver
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Solver.Ring.AlmostCommutativeRing where
 

diff --git a/src/Algebra/Solver/Ring/Lemmas.agda b/src/Algebra/Solver/Ring/Lemmas.agda
@@ -6,7 +6,7 @@
 
 -- Note that these proofs use all "almost commutative ring" properties.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 open import Algebra.Solver.Ring.AlmostCommutativeRing

diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
@@ -5,7 +5,7 @@
 -- coefficient "ring"
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 import Algebra.Operations.Semiring as SemiringOps

diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
@@ -9,7 +9,7 @@
 -- characteristic 0.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra
 

diff --git a/src/Algebra/Solver/Ring/Simple.agda b/src/Algebra/Solver/Ring/Simple.agda
@@ -5,7 +5,7 @@
 -- decidable equality
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Relation.Binary

diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
@@ -5,7 +5,7 @@
 -- etc.)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 

diff --git a/src/Category/Applicative.agda b/src/Category/Applicative.agda
@@ -7,7 +7,7 @@
 -- Note that currently the applicative functor laws are not included
 -- here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Applicative where
 

diff --git a/src/Category/Applicative/Indexed.agda b/src/Category/Applicative/Indexed.agda
@@ -7,7 +7,7 @@
 -- Note that currently the applicative functor laws are not included
 -- here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Applicative.Indexed where
 

diff --git a/src/Category/Applicative/Predicate.agda b/src/Category/Applicative/Predicate.agda
@@ -7,7 +7,7 @@
 -- Note that currently the applicative functor laws are not included
 -- here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Applicative.Predicate where
 

diff --git a/src/Category/Comonad.agda b/src/Category/Comonad.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the monad laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Comonad where
 

diff --git a/src/Category/Functor.agda b/src/Category/Functor.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the functor laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Functor where
 

diff --git a/src/Category/Functor/Predicate.agda b/src/Category/Functor/Predicate.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the functor laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Functor.Predicate where
 

diff --git a/src/Category/Monad.agda b/src/Category/Monad.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the monad laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad where
 

diff --git a/src/Category/Monad/Continuation.agda b/src/Category/Monad/Continuation.agda
@@ -4,7 +4,7 @@
 -- A delimited continuation monad
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.Continuation where
 

diff --git a/src/Category/Monad/Indexed.agda b/src/Category/Monad/Indexed.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the monad laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.Indexed where
 

diff --git a/src/Category/Monad/Partiality.agda b/src/Category/Monad/Partiality.agda
@@ -4,7 +4,7 @@
 -- The partiality monad
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.Partiality where
 

diff --git a/src/Category/Monad/Partiality/All.agda b/src/Category/Monad/Partiality/All.agda
@@ -4,7 +4,7 @@
 -- An All predicate for the partiality monad
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.Partiality.All where
 

diff --git a/src/Category/Monad/Predicate.agda b/src/Category/Monad/Predicate.agda
@@ -6,7 +6,7 @@
 
 -- Note that currently the monad laws are not included here.
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.Predicate where
 

diff --git a/src/Category/Monad/State.agda b/src/Category/Monad/State.agda
@@ -4,7 +4,7 @@
 -- The state monad
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Category.Monad.State where
 

diff --git a/src/Codata/Cofin.agda b/src/Codata/Cofin.agda
@@ -4,7 +4,7 @@
 -- "Finite" sets indexed on coinductive "natural" numbers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Codata.Cofin where
 

diff --git a/src/Codata/Cofin/Literals.agda b/src/Codata/Cofin/Literals.agda
@@ -4,7 +4,7 @@
 -- Conat Literals
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Codata.Cofin.Literals where
 

diff --git a/src/Codata/Colist.agda b/src/Codata/Colist.agda
@@ -4,7 +4,7 @@
 -- The Colist type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Codata.Colist where