------------------------------------------------------------------------
-- The Agda standard library
--
-- M-types (the dual of W-types)
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible --guardedness #-}
module Codata.Musical.M where
open import Codata.Musical.Notation using (♭; ∞; ♯_)
open import Level using (Level; _⊔_)
open import Data.Product.Base hiding (map)
open import Data.Container.Core as C hiding (map)
-- The family of M-types.
data M {s p} (C : Container s p) : Set (s ⊔ p) where
inf : ⟦ C ⟧ (∞ (M C)) → M C
-- Projections.
module _ {s p} (C : Container s p) where
head : M C → Shape C
head (inf (x , _)) = x
tail : (x : M C) → Position C (head x) → M C
tail (inf (x , f)) b = ♭ (f b)
-- map
module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
(m : C₁ ⇒ C₂) where
map : M C₁ → M C₂
map (inf (x , f)) = inf (shape m x , λ p → ♯ map (♭ (f (position m p))))
-- unfold
module _ {s p ℓ} {C : Container s p} (open Container C)
{S : Set ℓ} (alg : S → ⟦ C ⟧ S) where
unfold : S → M C
unfold seed = let (x , f) = alg seed in
inf (x , λ p → ♯ unfold (f p))
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