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