Agda.Interaction.Library.Base

Basic data types for library management.

Documentation

type LibName = String

A symbolic library name.

libNameForCurrentDir :: LibName

The special name "." is used to indicated that the current directory should count as a project root.

data AgdaLibFile

Content of a .agda-lib file.

Constructors

AgdaLibFile

Fields

• _libName :: LibName

  The symbolic name of the library.

• _libFile :: FilePath

  Path to this .agda-lib file (not content of the file).

• _libIncludes :: [FilePath]

  Roots where to look for the modules of the library.

• _libDepends :: [LibName]

  Dependencies.

Instances

Show AgdaLibFile

Defined in Agda.Interaction.Library.Base

Methods

showsPrec :: Int -> AgdaLibFile -> ShowS

show :: AgdaLibFile -> String

showList :: [AgdaLibFile] -> ShowS

emptyLibFile :: AgdaLibFile

libName :: Lens' LibName AgdaLibFile

Lenses for AgdaLibFile

libFile :: Lens' FilePath AgdaLibFile

libIncludes :: Lens' [FilePath] AgdaLibFile

libDepends :: Lens' [LibName] AgdaLibFile