Rename Set to Type in examples

Author: HeinrichApfelmus

tutorials/example-basics/HelloWorld.agda

@@ -7,7 +7,7 @@ Entry = Int × List String
 
 
 --defining a datatype
-data Tree (a : Set) : Set where
+data Tree (a : Type) : Type where
     Leaf   : a → Tree a
     Branch : a → Tree a → Tree a → Tree a
 

tutorials/example-proofs/Ascending.agda

@@ -14,7 +14,7 @@ isAscending (x ∷ y ∷ xs) = if x <= y then isAscending (y ∷ xs) else False
 {-# COMPILE AGDA2HS isAscending #-}
 
 -- data type defining a postulate of ascending order on lists
-data IsAscending₂ {a : Set} ⦃ iOrdA : Ord a ⦄ : List a → Set where
+data IsAscending₂ {a : Type} ⦃ iOrdA : Ord a ⦄ : List a → Type where
     Empty : IsAscending₂ []
     OneElem : (x : a) →  IsAscending₂ (x ∷ [])
     ManyElem : (x y : a) (xs : List a) 

tutorials/example-proofs/Triangle.agda

@@ -10,7 +10,7 @@ countBiggerThan xs b = length (filter (λ x → (x >= b)) xs)
 {-# COMPILE AGDA2HS countBiggerThan #-}
 
 -- Triangle data type deinfition
-data Triangle : Set where
+data Triangle : Type where
     MkTriangle : (alpha beta gamma : Nat)
         → ⦃ @0 h₁ : (((alpha + beta + gamma) == 180) ≡ True ) ⦄
         → @0 ⦃ ((countBiggerThan

tutorials/example-structure/src/agda/Definition.agda

@@ -2,7 +2,7 @@ module Definition where
 
 open import Haskell.Prelude
 
-data CountDown : Set where
+data CountDown : Type where
     MkCountdown : (start  : Int)
             → {{ @0 h : ((start > 0) ≡ True) }}
             → CountDown