------------------------------------------------------------------------
-- The Agda standard library
--
-- Greatest fixpoint for indexed containers - using guardedness
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible --guardedness #-}
module Data.Container.Indexed.Fixpoints.Guarded where
open import Level using (Level; _⊔_)
open import Codata.Musical.M.Indexed using (M)
open import Data.Container.Indexed using (Container)
open import Relation.Unary using (Pred)
private
variable
o c r : Level
O : Set o
-- The least fixpoint can be found in `Data.Container`
open Data.Container.Indexed public
using (μ)
-- This lives in its own module due to its use of guardedness.
ν : Container O O c r → Pred O _
ν = M
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