{- |
Module: Agda.Unused.Types.Access

Access modifiers indicating whether an item is public or private.
-}
module Agda.Unused.Types.Access

  ( -- * Definition
    
    Access(..)

    -- * Interface

  , access
   
    -- * Conversion

  , fromAccess

  ) where

import qualified Agda.Syntax.Common
  as C

-- | An access modifier.
data Access where

  Private
    :: Access

  Public
    :: Access

  deriving Int -> Access -> ShowS
[Access] -> ShowS
Access -> String
(Int -> Access -> ShowS)
-> (Access -> String) -> ([Access] -> ShowS) -> Show Access
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Access] -> ShowS
$cshowList :: [Access] -> ShowS
show :: Access -> String
$cshow :: Access -> String
showsPrec :: Int -> Access -> ShowS
$cshowsPrec :: Int -> Access -> ShowS
Show

-- | Elimination rule for 'Access'.
access
  :: a
  -> a
  -> Access
  -> a
access :: a -> a -> Access -> a
access x :: a
x _ Private
  = a
x
access _ y :: a
y Public
  = a
y

-- | Conversion from Agda access type.
fromAccess
  :: C.Access
  -> Access
fromAccess :: Access -> Access
fromAccess (C.PrivateAccess _)
  = Access
Private
fromAccess C.PublicAccess
  = Access
Public