Update examples for Agda 2.5.4.2, stdlib 0.17

examples/Filter/Base.agda

@@ -1,18 +1,17 @@
 module Filter.Base where
 
 open import Data.Nat using (ℕ ; _<_)
-open import Data.Product
-open import Data.Unit
-open import Level using (Lift ; lift)
+open import Data.Product using (proj₁ ; proj₂ ; _,_)
+open import Data.Unit using (⊤)
 open import Relation.Binary.PropositionalEquality
   using (_≡_ ; _≢_)
 open import Size using (Size ; ↑_)
 
 open import Coinduction.WellFounded
 
 
-StreamC : ∀ {a} → Set a → Container a
-StreamC A = A ▷ (λ _ → Lift ⊤)
+StreamC : ∀ {a} → Set a → Container a _
+StreamC A = A ▷ (λ _ → ⊤)
 
 
 Stream : ∀ {a} → Set a → Size → Set a
@@ -26,7 +25,7 @@ module _ {a} {A : Set a} where
 
 
   tail : ∀ {s} → Stream A (↑ s) → Stream A s
-  tail xs = proj₂ (inf xs) (lift tt)
+  tail xs = proj₂ (inf xs) _
 
 
   cons : ∀ {s} → A → Stream A s → Stream A (↑ s)

examples/Filter/M.agda

@@ -5,8 +5,8 @@ open import Data.Empty
 open import Data.Nat using (_<_)
 open import Data.Product
 open import Function
-open import Induction.Nat using (<-well-founded)
-open import Induction.WellFounded using (Well-founded ; module Inverse-image)
+open import Induction.Nat using (<-wellFounded)
+open import Induction.WellFounded using (WellFounded ; module Inverse-image)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality using
   (_≡_ ; refl ; inspect ; [_] ; Extensionality)
@@ -24,8 +24,8 @@ module _ {a} {A : Set a} where
   xs <[ p ] ys = dist p xs < dist p ys
 
 
-  <[p]-wf : ∀ {p} → Well-founded _<[ p ]_
-  <[p]-wf {p} = Inverse-image.well-founded (dist p) <-well-founded
+  <[p]-wf : ∀ {p} → WellFounded _<[ p ]_
+  <[p]-wf {p} = Inverse-image.wellFounded (dist p) <-wellFounded
 
 
   module _ (p : A → Bool) where

examples/Filter/Properties.agda

@@ -111,8 +111,8 @@ module WithM {a : Level} where
     filter-unfold′ : ∀ xs → filter p xs ≡ filter-body p xs
     filter-unfold′ xs = ≅-to-≡ (≅M⇒≅ M-ext ≅-ext (filter-unfold p xs))
       where
-        postulate M-ext : M-Extensionality lzero a a ∞
-        postulate ≅-ext : Het.Extensionality a a
+        postulate M-ext : M-Extensionality lzero a lzero ∞
+        postulate ≅-ext : Het.Extensionality lzero a
 
 
     filter-⊆F : ∀ {t}

examples/Graph/Base.agda

@@ -108,7 +108,7 @@ nu-unfold-contractive c@(var _) = c
 nu-unfold-contractive c@(nu _ c') = subst-preserves-Contractive c' c
 
 
--- Closedness 
+-- Closedness
 
 
 data ClosedWrt : List Var → LoopyTree → Set where
@@ -207,8 +207,8 @@ _<<<_ : Rel LoopyTreeWf lzero
 _<<<_ = _<_ on nu-prefix-length ∘ LoopyTreeWf.tree
 
 
-<<<-wf : Well-founded _<<<_
-<<<-wf = Inverse-image.well-founded _ <-well-founded
+<<<-wf : WellFounded _<<<_
+<<<-wf = Inverse-image.wellFounded _ <-wellFounded
 
 
 nu-unfold-wf : LoopyTreeWf → LoopyTreeWf
@@ -245,7 +245,7 @@ fmap-GraphF f (branch l r) = branch (f l) (f r)
 -- Graphs via M-types
 
 
-GraphMF : Container _
+GraphMF : Container _ _
 GraphMF = Shape ▷ Position
   module _ where
     data Shape : Set where

examples/Graph/List.agda

@@ -3,7 +3,8 @@ module Graph.List where
 open import Data.List public
 open import Data.List.Any public using (here ; there)
 open import Data.List.Membership.Propositional public using (_∈_)
-open import Data.List.Relation.Sublist.Propositional public using (_⊆_)
+open import Data.List.Relation.Subset.Propositional public using (_⊆_)
+
 open import Relation.Binary.PropositionalEquality using (refl)
 
 ∷-⊆ : ∀ {a} {A : Set a} {xs ys} {x : A} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)

examples/Graph/Special.agda

@@ -25,7 +25,7 @@ open Graph∞
 
 module _
   {lin l<} {In : Set lin} {_<_ : Rel In l<}
-  (<-wf : Well-founded _<_)
+  (<-wf : WellFounded _<_)
   (F : ∀ {t}
     → (x : In)
     → (In → Graph∞ t)

examples/Runs/Base.agda

@@ -21,7 +21,7 @@ module Stream where
   open import Coinduction.WellFounded
 
 
-  StreamC : Set → Container lzero
+  StreamC : Set → Container lzero lzero
   StreamC A = A ▷ (λ _ → ⊤)
 
 

examples/Runs/M.agda

@@ -7,8 +7,8 @@ open import Data.Nat
 open import Data.Product
 open import Data.Unit using (⊤ ; tt)
 open import Function using (_∘_ ; _on_)
-open import Induction.Nat using (<-well-founded)
-open import Induction.WellFounded using (Well-founded ; module Inverse-image)
+open import Induction.Nat using (<-wellFounded)
+open import Induction.WellFounded using (WellFounded ; module Inverse-image)
 open import Level using () renaming (zero to lzero ; suc to lsuc)
 open import Relation.Nullary using (Dec ; yes ; no)
 open import Relation.Nullary.Decidable using (⌊_⌋)
@@ -22,7 +22,6 @@ open import Size
 open import Coinduction.WellFounded
 import Coinduction.WellFounded.Indexed as Ix
 open import Runs.Base
-open import Runs.Nat
 
 
 -- # Well-founded relation
@@ -32,8 +31,8 @@ _<<_ : ∀ {A : Set} → Rel (Stream ℕ ∞ × A) lzero
 _<<_ (xs , _) (ys , _) = head xs < head ys
 
 
-<<-wf : ∀ {A} → Well-founded (_<<_ {A = A})
-<<-wf = Inverse-image.well-founded _ <-well-founded
+<<-wf : ∀ {A} → WellFounded (_<<_ {A = A})
+<<-wf = Inverse-image.wellFounded _ <-wellFounded
 
 
 -- # Definition of runs
@@ -171,8 +170,8 @@ module Internal₁ where
   _<<<_ : ∀ {ys ys′} → In ys → In ys′ → Set
   x <<< y = head (In.xs x) < head (In.xs y)
 
-  <<<-wf : ∀ {ys} → Well-founded {A = In ys} _<<<_
-  <<<-wf = Inverse-image.well-founded _ <-well-founded
+  <<<-wf : ∀ {ys} → WellFounded {A = In ys} _<<<_
+  <<<-wf = Inverse-image.wellFounded _ <-wellFounded
 
   Out : ∀ {ys} → In ys → Stream (List ℕ) ∞
   Out (build-In xs run _ _) = runs′ (xs , run)