------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-empty AVL trees, where equality for keys is propositional equality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
module Data.Tree.AVL.NonEmpty.Propositional
{k r} {Key : Set k} {_<_ : Rel Key r}
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
open import Level using (Level; _⊔_)
open import Relation.Binary.Bundles using (StrictTotalOrder)
private
strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
open import Data.Tree.AVL.Value (StrictTotalOrder.Eq.setoid strictTotalOrder)
import Data.Tree.AVL.NonEmpty strictTotalOrder as AVL⁺
Tree⁺ : ∀ {v} (V : Key → Set v) → Set (k ⊔ v ⊔ r)
Tree⁺ V = AVL⁺.Tree⁺ λ where
.Value.family → V
.Value.respects refl t → t
open AVL⁺ hiding (Tree⁺) public
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