------------------------------------------------------------------------
-- Safe modules that use --erased-cubical and --guardedness
------------------------------------------------------------------------

{-# OPTIONS --safe --erased-cubical --guardedness #-}

module README.Safe.Cubical.Erased.Guardedness where

-- M-types for indexed containers, defined coinductively (in Cubical
-- Agda).

import Container.Indexed.Variant.M.Codata
import Container.Indexed.M.Codata