Source code on Github
{-# OPTIONS --with-K #-}
module Prelude.Irrelevance.List where

open import Prelude.Irrelevance.List.Unique public
open import Prelude.Irrelevance.List.Membership public
open import Prelude.Irrelevance.List.Permutation public
open import Prelude.Irrelevance.List.Subset public
open import Prelude.Irrelevance.List.Collections