module Prelude where

open import Agda.Primitive      public

open import Prelude.Unit        public
open import Prelude.Empty       public
open import Prelude.Function    public
open import Prelude.Char        public
open import Prelude.String      public
open import Prelude.Bool        public
open import Prelude.Nat         public
open import Prelude.Product     public
open import Prelude.Sum         public
open import Prelude.List        public
open import Prelude.Maybe       public
open import Prelude.Fin         public
open import Prelude.Vec         public
open import Prelude.Semiring    public
open import Prelude.Number      public
open import Prelude.Erased      public

open import Prelude.Equality    public
open import Prelude.Decidable   public
open import Prelude.Functor     public
open import Prelude.Applicative public
open import Prelude.Monad       public
open import Prelude.Show        public
open import Prelude.Ord         public

open import Prelude.IO          public

open import Prelude.Equality.Unsafe public using (eraseEquality)

infixr  _::_
pattern _::_ x xs = x ∷ xs