{- |
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

-- ## Definition

-- | 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

-- ## Interface

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

-- ## Conversion

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