fix compilation with agda 2.5.3, agda-stdlib 0.14
[~helmut/bidiragda.git] / Examples.agda
index cfe9432..bedad5a 100644 (file)
@@ -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