diff options
Diffstat (limited to 'Examples.agda')
| -rw-r--r-- | Examples.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Examples.agda b/Examples.agda index cfe9432..bedad5a 100644 --- a/Examples.agda +++ b/Examples.agda @@ -2,7 +2,7 @@ module Examples where open import Data.Maybe using (just ; nothing) open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉) -open import Data.Nat.Properties using (cancel-+-left) +open import Data.Nat.Properties using (cancel-+-left ; ≤-decTotalOrder) import Algebra.Structures open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_) open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map) @@ -19,7 +19,7 @@ open GetTypes.PartialVecVec using (Get) open FreeTheorems.PartialVecVec using (assume-get) open BFF.PartialVecBFF using (bff) -ℕ-decSetoid = Relation.Binary.DecTotalOrder.Eq.decSetoid Data.Nat.decTotalOrder +ℕ-decSetoid = Relation.Binary.DecTotalOrder.Eq.decSetoid ≤-decTotalOrder reverse' : Get reverse' = assume-get id id reverse |