Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe
Language | Haskell2010

Agda.Interaction.Library.Base

Description

Basic data types for library management.

Synopsis

- type LibName = String
- libNameForCurrentDir :: LibName
- data AgdaLibFile = AgdaLib {
  - libName :: LibName
  - libFile :: FilePath
  - libIncludes :: [FilePath]
  - libDepends :: [LibName]
  }
- emptyLibFile :: AgdaLibFile

# Documentation

type LibName = String Source #

A symbolic library name.

libNameForCurrentDir :: LibName Source #

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

data AgdaLibFile Source #

Content of a `.agda-lib` file.

Constructors

AgdaLib |

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 Source # |
Instance details Defined in Agda.Interaction.Library.Base Methods showsPrec :: Int -> AgdaLibFile -> ShowS Source # show :: AgdaLibFile -> String Source # showList :: [AgdaLibFile] -> ShowS Source #

emptyLibFile :: AgdaLibFile Source #