Idris.Package.Types

Definitions

data PkgVersion : Type

Totality: total
Visibility: public export
Constructor: 

MkPkgVersion : List1 Nat -> PkgVersion

Hints:

Eq PkgVersion

Ord PkgVersion

Pretty Void PkgVersion

Show PkgVersion

ToJson PkgVersion

record PkgVersionBounds : Type

Totality: total
Visibility: public export
Constructor: 

MkPkgVersionBounds : Maybe PkgVersion -> Bool -> Maybe PkgVersion -> Bool -> PkgVersionBounds

Projections:

.lowerBound : PkgVersionBounds -> Maybe PkgVersion

.lowerInclusive : PkgVersionBounds -> Bool

.upperBound : PkgVersionBounds -> Maybe PkgVersion

.upperInclusive : PkgVersionBounds -> Bool

Hints:

Pretty Void PkgVersionBounds

Show PkgVersionBounds

ToJson PkgVersionBounds

.lowerBound : PkgVersionBounds -> Maybe PkgVersion

Totality: total
Visibility: public export

lowerBound : PkgVersionBounds -> Maybe PkgVersion

Totality: total
Visibility: public export

.lowerInclusive : PkgVersionBounds -> Bool

Totality: total
Visibility: public export

lowerInclusive : PkgVersionBounds -> Bool

Totality: total
Visibility: public export

.upperBound : PkgVersionBounds -> Maybe PkgVersion

Totality: total
Visibility: public export

upperBound : PkgVersionBounds -> Maybe PkgVersion

Totality: total
Visibility: public export

.upperInclusive : PkgVersionBounds -> Bool

Totality: total
Visibility: public export

upperInclusive : PkgVersionBounds -> Bool

Totality: total
Visibility: public export

anyBounds : PkgVersionBounds

Totality: total
Visibility: export

exactBounds : Maybe PkgVersion -> PkgVersionBounds

Totality: total
Visibility: export

current : PkgVersionBounds

Totality: total
Visibility: export

defaultVersion : PkgVersion

Totality: total
Visibility: export

inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool

Totality: total
Visibility: export

inBounds : Version -> PkgVersionBounds -> Bool

  Check if a Version is within the bounds of a PkgVersionBounds.
  
  In addition to comparing major, minor, and patch version numbers,
  a Version with a tag is always considered larger than one with the
  same major, minor, and patch numbers but no tag.
  
  Therefore, Version 0.1.0-abcd will be within the bounds >0.1.0 && <0.2.0.
  Similarly, Version 0.2.0-abcd will be _outside_ the bounds
  >0.1.0 && <=0.2.0.

Totality: total
Visibility: export

record Depends : Type

Totality: total
Visibility: public export
Constructor: 

MkDepends : String -> PkgVersionBounds -> Depends

Projections:

.pkgbounds : Depends -> PkgVersionBounds

.pkgname : Depends -> String

Hints:

Pretty Void Depends

Show Depends

ToJson Depends

.pkgname : Depends -> String

Totality: total
Visibility: public export

pkgname : Depends -> String

Totality: total
Visibility: public export

.pkgbounds : Depends -> PkgVersionBounds

Totality: total
Visibility: public export

pkgbounds : Depends -> PkgVersionBounds

Totality: total
Visibility: public export

record PkgDesc : Type

Totality: total
Visibility: public export
Constructor: 

MkPkgDesc : String -> Maybe PkgVersion -> Maybe PkgVersionBounds -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> List Depends -> List (ModuleIdent, String) -> Maybe (ModuleIdent, String) -> Maybe String -> Maybe (FC, String) -> Maybe String -> Maybe String -> Maybe String -> Maybe (FC, String) -> Maybe (FC, String) -> Maybe (FC, String) -> Maybe (FC, String) -> Maybe (FC, String) -> Maybe (FC, String) -> PkgDesc

Projections:

.authors : PkgDesc -> Maybe String

.brief : PkgDesc -> Maybe String

.bugtracker : PkgDesc -> Maybe String

.builddir : PkgDesc -> Maybe String

.depends : PkgDesc -> List Depends

.executable : PkgDesc -> Maybe String

.homepage : PkgDesc -> Maybe String

.langversion : PkgDesc -> Maybe PkgVersionBounds

.license : PkgDesc -> Maybe String

.mainmod : PkgDesc -> Maybe (ModuleIdent, String)

.maintainers : PkgDesc -> Maybe String

.modules : PkgDesc -> List (ModuleIdent, String)

.name : PkgDesc -> String

.options : PkgDesc -> Maybe (FC, String)

.outputdir : PkgDesc -> Maybe String

.postbuild : PkgDesc -> Maybe (FC, String)

.postclean : PkgDesc -> Maybe (FC, String)

.postinstall : PkgDesc -> Maybe (FC, String)

.prebuild : PkgDesc -> Maybe (FC, String)

.preclean : PkgDesc -> Maybe (FC, String)

.preinstall : PkgDesc -> Maybe (FC, String)

.readme : PkgDesc -> Maybe String

.sourcedir : PkgDesc -> Maybe String

.sourceloc : PkgDesc -> Maybe String

.version : PkgDesc -> Maybe PkgVersion

Hints:

Pretty Void PkgDesc

Show PkgDesc

.name : PkgDesc -> String

Totality: total
Visibility: public export

name : PkgDesc -> String

Totality: total
Visibility: public export

.version : PkgDesc -> Maybe PkgVersion

Totality: total
Visibility: public export

version : PkgDesc -> Maybe PkgVersion

Totality: total
Visibility: public export

.langversion : PkgDesc -> Maybe PkgVersionBounds

Totality: total
Visibility: public export

langversion : PkgDesc -> Maybe PkgVersionBounds

Totality: total
Visibility: public export

.authors : PkgDesc -> Maybe String

Totality: total
Visibility: public export

authors : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.maintainers : PkgDesc -> Maybe String

Totality: total
Visibility: public export

maintainers : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.license : PkgDesc -> Maybe String

Totality: total
Visibility: public export

license : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.brief : PkgDesc -> Maybe String

Totality: total
Visibility: public export

brief : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.readme : PkgDesc -> Maybe String

Totality: total
Visibility: public export

readme : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.homepage : PkgDesc -> Maybe String

Totality: total
Visibility: public export

homepage : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.sourceloc : PkgDesc -> Maybe String

Totality: total
Visibility: public export

sourceloc : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.bugtracker : PkgDesc -> Maybe String

Totality: total
Visibility: public export

bugtracker : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.depends : PkgDesc -> List Depends

Totality: total
Visibility: public export

depends : PkgDesc -> List Depends

Totality: total
Visibility: public export

.modules : PkgDesc -> List (ModuleIdent, String)

Totality: total
Visibility: public export

modules : PkgDesc -> List (ModuleIdent, String)

Totality: total
Visibility: public export

.mainmod : PkgDesc -> Maybe (ModuleIdent, String)

Totality: total
Visibility: public export

mainmod : PkgDesc -> Maybe (ModuleIdent, String)

Totality: total
Visibility: public export

.executable : PkgDesc -> Maybe String

Totality: total
Visibility: public export

executable : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.options : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

options : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.sourcedir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

sourcedir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.builddir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

builddir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.outputdir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

outputdir : PkgDesc -> Maybe String

Totality: total
Visibility: public export

.prebuild : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

prebuild : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.postbuild : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

postbuild : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.preinstall : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

preinstall : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.postinstall : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

postinstall : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.preclean : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

preclean : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

.postclean : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

postclean : PkgDesc -> Maybe (FC, String)

Totality: total
Visibility: public export

initPkgDesc : String -> PkgDesc

Totality: total
Visibility: export

record CSS : Type

Totality: total
Visibility: public export
Constructor: 

MkCSS : String -> String -> CSS

Projections:

.filename : CSS -> String

.stylename : CSS -> String

.stylename : CSS -> String

Totality: total
Visibility: public export

stylename : CSS -> String

Totality: total
Visibility: public export

.filename : CSS -> String

Totality: total
Visibility: public export

filename : CSS -> String

Totality: total
Visibility: public export

cssFiles : List CSS

Totality: total
Visibility: export