diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2018-01-01 19:51:00 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2018-01-01 19:51:00 +0100 |
| commit | ab79a2e7b7c10306493cb6e61eb10f3b4e114cf3 (patch) | |
| tree | 923efedbb0b74075d8efb66ba4b5b33dd4ed3cc2 /Examples.agda | |
| parent | ad721d4770c02769a9b7afab90160d1818afe1d6 (diff) | |
| download | bidiragda-ab79a2e7b7c10306493cb6e61eb10f3b4e114cf3.tar.gz | |
fix compilation with agda 2.5.3, agda-stdlib 0.14
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 |