Agda.Unused.Types.Access

Access modifiers indicating whether an item is public or private.

Definition

data Access where

An access modifier.

Constructors

Private :: Access

Public :: Access

Instances

Show Access

Defined in Agda.Unused.Types.Access

Methods

showsPrec :: Int -> Access -> ShowS

show :: Access -> String

showList :: [Access] -> ShowS

Interface

access :: a -> a -> Access -> a

Elimination rule for Access.

Conversion

fromAccess :: Access -> Access

Conversion from Agda access type.