------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Erased where

{-# WARNING_ON_IMPORT
"Data.Erased was deprecated in v2.0.
Use Data.Irrelevant instead."
#-}

open import Data.Irrelevant public
  using ([_]; map; pure; _<*>_; _>>=_; zipWith)
  renaming
  ( Irrelevant to Erased
  ; irrelevant to erased
  )