summaryrefslogtreecommitdiff
path: root/src/Data/BoundedVec.agda
diff options
context:
space:
mode:
authorSean Whitton <spwhitton@spwhitton.name>2018-11-23 17:29:46 -0700
committerSean Whitton <spwhitton@spwhitton.name>2018-11-23 17:29:46 -0700
commit5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch)
treecea89f085c1382f1567ff71a30b6f953708dc6a9 /src/Data/BoundedVec.agda
parent5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff)
parenta19b25a865b2000bbd3acd909f5951a5407c1eec (diff)
Merge tag 'upstream/0.17'
Upstream version 0.17 # gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST # gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240 # gpg: issuer "spwhitton@spwhitton.name" # gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate] # Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B # Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
Diffstat (limited to 'src/Data/BoundedVec.agda')
-rw-r--r--src/Data/BoundedVec.agda4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Data/BoundedVec.agda b/src/Data/BoundedVec.agda
index 6359af2..cd88d6d 100644
--- a/src/Data/BoundedVec.agda
+++ b/src/Data/BoundedVec.agda
@@ -13,8 +13,8 @@ open import Data.List.Base as List using (List)
open import Data.Vec as Vec using (Vec)
import Data.BoundedVec.Inefficient as Ineff
open import Relation.Binary.PropositionalEquality
-open import Data.Nat.Properties
-open SemiringSolver
+open import Data.Nat.Solver
+open +-*-Solver
------------------------------------------------------------------------
-- The type