------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists which contain every element of a given type
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Data.List.Base using (List)
open import Level
open import Relation.Binary.Bundles using (Setoid)
module Data.List.Relation.Unary.Enumerates.Setoid
{a ℓ} (S : Setoid a ℓ) where
open Setoid S renaming (Carrier to A)
open import Data.List.Membership.Setoid S
------------------------------------------------------------------------
-- Definition
IsEnumeration : List A → Set (a ⊔ ℓ)
IsEnumeration xs = ∀ x → x ∈ xs
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4