------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation with respect to a
-- setoid which is decidable. This is a generalisation of what is
-- commonly known as Order Preserving Embeddings (OPE).
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecSetoid; DecPoset)
open import Relation.Binary.Structures
using (IsDecPartialOrder)
open import Relation.Binary.Definitions using (Decidable)
module Data.List.Relation.Binary.Sublist.DecSetoid
{c ℓ} (S : DecSetoid c ℓ) where
import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEquality
import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
as HeterogeneousProperties
open import Level using (_⊔_)
open DecSetoid S
open DecSetoidEquality S
infix 4 _⊆?_
------------------------------------------------------------------------
-- Re-export core definitions
open SetoidSublist setoid public
------------------------------------------------------------------------
-- Additional relational properties
_⊆?_ : Decidable _⊆_
_⊆?_ = HeterogeneousProperties.sublist? _≟_
⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
⊆-isDecPartialOrder = record
{ isPartialOrder = ⊆-isPartialOrder
; _≟_ = _≋?_
; _≤?_ = _⊆?_
}
⊆-decPoset : DecPoset c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-decPoset = record
{ isDecPartialOrder = ⊆-isDecPartialOrder
}
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