From ab79a2e7b7c10306493cb6e61eb10f3b4e114cf3 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 1 Jan 2018 19:51:00 +0100 Subject: fix compilation with agda 2.5.3, agda-stdlib 0.14 --- Examples.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Examples.agda') 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 -- cgit v1.2.3