New upstream version 0.17

1 files changed, 11 insertions, 11 deletions

diff --git a/src/Data/Star/Vec.agda b/src/Data/Star/Vec.agda
index e7e0a53..e10b941 100644
--- a/src/Data/Star/Vec.agda
+++ b/src/Data/Star/Vec.agda
@@ -1,12 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Vectors defined in terms of Data.Star
+-- Vectors defined in terms of the reflexive-transitive closure, Star
 ------------------------------------------------------------------------
 
 module Data.Star.Vec where
 
-open import Data.Star
 open import Data.Star.Nat
 open import Data.Star.Fin using (Fin)
 open import Data.Star.Decoration
@@ -14,6 +13,7 @@ open import Data.Star.Pointer as Pointer hiding (lookup)
 open import Data.Star.List using (List)
 open import Relation.Binary
 open import Relation.Binary.Consequences
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 open import Function
 open import Data.Unit
 
@@ -21,45 +21,45 @@ open import Data.Unit
 -- information (i.e. elements).
 
 Vec : Set → ℕ → Set
-Vec a = All (λ _ → a)
+Vec A = All (λ _ → A)
 
 -- Nil and cons.
 
-[] : ∀ {a} → Vec a zero
+[] : ∀ {A} → Vec A zero
 [] = ε
 
 infixr 5 _∷_
 
-_∷_ : ∀ {a n} → a → Vec a n → Vec a (suc n)
+_∷_ : ∀ {A n} → A → Vec A n → Vec A (suc n)
 x ∷ xs = ↦ x ◅ xs
 
 -- Projections.
 
-head : ∀ {a n} → Vec a (1# + n) → a
+head : ∀ {A n} → Vec A (1# + n) → A
 head (↦ x ◅ _) = x
 
-tail : ∀ {a n} → Vec a (1# + n) → Vec a n
+tail : ∀ {A n} → Vec A (1# + n) → Vec A n
 tail (↦ _ ◅ xs) = xs
 
 -- Append.
 
 infixr 5 _++_
 
-_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
+_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
 _++_ = _◅◅◅_
 
 -- Safe lookup.
 
-lookup : ∀ {a n} → Fin n → Vec a n → a
+lookup : ∀ {A n} → Fin n → Vec A n → A
 lookup i xs with Pointer.lookup i xs
 ... | result _ x = x
 
 ------------------------------------------------------------------------
 -- Conversions
 
-fromList : ∀ {a} → (xs : List a) → Vec a (length xs)
+fromList : ∀ {A} → (xs : List A) → Vec A (length xs)
 fromList ε        = []
 fromList (x ◅ xs) = x ∷ fromList xs
 
-toList : ∀ {a n} → Vec a n → List a
+toList : ∀ {A n} → Vec A n → List A
 toList = gmap (const tt) decoration