Rename Set to Type in tests

Author: HeinrichApfelmus

test/BangPatterns.agda

@@ -19,13 +19,13 @@ foldl'' f (! x0) (x ∷ xs) = foldl'' f (! f x0 x) xs
 
 {-# COMPILE AGDA2HS foldl'' #-}
 
-data LazyMaybe (a : Set ℓ) : Set ℓ where
+data LazyMaybe (a : Type ℓ) : Type ℓ where
   LazyNothing : LazyMaybe a
   LazyJust    : a → LazyMaybe a
 
 {-# COMPILE AGDA2HS LazyMaybe #-}
 
-data StrictMaybe (a : Set ℓ) : Set ℓ where
+data StrictMaybe (a : Type ℓ) : Type ℓ where
   StrictNothing : StrictMaybe a
   StrictJust    : Strict a → StrictMaybe a
 

test/CanonicalInstance.agda

@@ -4,14 +4,14 @@ module _ where
 
 open import Haskell.Prelude
 
-record ClassA (a : Set) : Set where
+record ClassA (a : Type) : Type where
   field
     myA : a
 
 open ClassA ⦃ ... ⦄ public
 {-# COMPILE AGDA2HS ClassA class #-}
 
-record ClassB (b : Set) : Set where
+record ClassB (b : Type) : Type where
   field
     overlap ⦃ super ⦄ : ClassA b
 {-# COMPILE AGDA2HS ClassB class #-}

test/Coerce.agda

@@ -1,9 +1,9 @@
 open import Haskell.Prelude
 
-data A : Set where
+data A : Type where
   MkA : Nat → A
 
-data B : Set where
+data B : Type where
   MkB : Nat → B
 
 postulate A≡B : A ≡ B

test/Coinduction.agda

@@ -5,7 +5,7 @@ module Coinduction where
 open import Haskell.Prelude
 open import Haskell.Prim.Thunk
 
-data Colist (a : Set) (@0 i : Size) : Set where
+data Colist (a : Type) (@0 i : Size) : Type where
   Nil  : Colist a i
   Cons : a -> Thunk (Colist a) i -> Colist a i
 

test/ConstrainedInstance.agda

@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-data D (a : Set) : Set where
+data D (a : Type) : Type where
   C : a → D a
 {-# COMPILE AGDA2HS D #-}
 

test/Cubical/StreamFusion.agda

@@ -2,15 +2,14 @@ module Cubical.StreamFusion where
 
 open import Haskell.Prelude
 
-open import Agda.Primitive
 open import Agda.Primitive.Cubical
 open import Agda.Builtin.Equality
 open import Agda.Builtin.Size
 
 variable
   @0 i : Size
 
-record Stream (a : Set) (@0 i : Size) : Set where
+record Stream (a : Type) (@0 i : Size) : Type where
   pattern; inductive; constructor _:>_
   field
     shead : a

test/CustomTuples.agda

@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record Σ (a : Set) (b : @0 a → Set) : Set where
+record Σ (a : Type) (b : @0 a → Type) : Type where
   constructor _,_
   field
     fst : a
@@ -13,7 +13,7 @@ test xy = fst xy + snd xy
 
 {-# COMPILE AGDA2HS test #-}
 
-record Stuff (a : Set) : Set where
+record Stuff (a : Type) : Type where
   no-eta-equality; pattern
   constructor stuff
   field
@@ -38,7 +38,7 @@ section = stuff 42
 
 {-# COMPILE AGDA2HS section #-}
 
-record NoStuff : Set where
+record NoStuff : Type where
   no-eta-equality; pattern
   constructor dontlook
 
@@ -50,7 +50,7 @@ bar dontlook = dontlook
 {-# COMPILE AGDA2HS bar #-}
 
 -- This is legal, basically the same as an unboxed record.
-record Legal (a : Set) : Set where
+record Legal (a : Type) : Type where
   constructor mkLegal
   field
     theA : a

test/Datatypes.agda

@@ -1,7 +1,7 @@
 
-open import Agda.Builtin.Bool
+open import Haskell.Prim using (Bool; Type)
 
-data Test : Set where
+data Test : Type where
   CTest : Bool -> @0 {Bool} -> Test
 {-# COMPILE AGDA2HS Test #-}
 

test/Default.agda

@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record HasDefault (a : Set) : Set where
+record HasDefault (a : Type) : Type where
   field
     theDefault : a
 open HasDefault {{...}}

test/DefaultMethods.agda

@@ -14,18 +14,18 @@ import Prelude hiding (Show, show, showsPrec, showList, Ord, (<), (>))
 
 -- ** Ord
 
-record Ord (a : Set) : Set where
+record Ord (a : Type) : Type where
   field
     _<_ _>_ : a → a → Bool
 
-record Ord₁ (a : Set) : Set where
+record Ord₁ (a : Type) : Type where
   field
     _<_ : a → a → Bool
 
   _>_ : a → a → Bool
   x > y = y < x
 
-record Ord₂ (a : Set) : Set where
+record Ord₂ (a : Type) : Type where
   field
     _>_ : a → a → Bool
 
@@ -46,7 +46,7 @@ instance
   OrdBool₀ ._>_ = Ord₁._>_ OB
 {-# COMPILE AGDA2HS OrdBool₀ #-}
 
-data Bool1 : Set where
+data Bool1 : Type where
   Mk1 : Bool -> Bool1
 {-# COMPILE AGDA2HS Bool1 #-}
 instance
@@ -58,7 +58,7 @@ instance
       ord₁ .Ord₁._<_ (Mk1 True)  _       = False
 {-# COMPILE AGDA2HS OrdBool₁ #-}
 
-data Bool2 : Set where
+data Bool2 : Type where
   Mk2 : Bool -> Bool2
 {-# COMPILE AGDA2HS Bool2 #-}
 instance
@@ -70,7 +70,7 @@ instance
       (Mk2 True)  <: _       = False
 {-# COMPILE AGDA2HS OrdBool₂ #-}
 
-data Bool3 : Set where
+data Bool3 : Type where
   Mk3 : Bool -> Bool3
 {-# COMPILE AGDA2HS Bool3 #-}
 instance
@@ -82,7 +82,7 @@ instance
       (Mk3 True)  <: _       = False
 {-# COMPILE AGDA2HS OrdBool₃ #-}
 
-data Bool4 : Set where
+data Bool4 : Type where
   Mk4 : Bool -> Bool4
 {-# COMPILE AGDA2HS Bool4 #-}
 lift4 : (Bool → Bool → a) → (Bool4 → Bool4 → a)
@@ -93,7 +93,7 @@ instance
   OrdBool₄ = record {Ord₁ (λ where .Ord₁._<_ → lift4 (λ x y → not x && y))}
 {-# COMPILE AGDA2HS OrdBool₄ #-}
 
-data Bool5 : Set where
+data Bool5 : Type where
   Mk5 : Bool -> Bool5
 {-# COMPILE AGDA2HS Bool5 #-}
 instance
@@ -105,7 +105,7 @@ instance
       (Mk5 True)  >: (Mk5 b) = not b
 {-# COMPILE AGDA2HS OrdBool₅ #-}
 
-data Bool6 : Set where
+data Bool6 : Type where
   Mk6 : Bool -> Bool6
 {-# COMPILE AGDA2HS Bool6 #-}
 instance
@@ -131,13 +131,13 @@ defaultShowList shows (x ∷ xs)
   ∘ showString "]"
 {-# COMPILE AGDA2HS defaultShowList #-}
 
-record Show (a : Set) : Set where
+record Show (a : Type) : Type where
   field
     show : a → String
     showsPrec : Int → a → ShowS
     showList : List a → ShowS
 
-record Show₁ (a : Set) : Set where
+record Show₁ (a : Type) : Type where
   field showsPrec : Int → a → ShowS
 
   show : a → String
@@ -146,7 +146,7 @@ record Show₁ (a : Set) : Set where
   showList : List a → ShowS
   showList = defaultShowList (showsPrec 0)
 
-record Show₂ (a : Set) : Set where
+record Show₂ (a : Type) : Type where
   field show : a → String
 
   showsPrec : Int → a → ShowS