Evince.SrcLoc

Definitions

record SrcLoc : Type

  A source file location (file path, line, column). Line and column
  are 0-indexed.

Totality: total
Visibility: public export
Constructor: 

MkSrcLoc : String -> Int -> Int -> SrcLoc

Projections:

.col : SrcLoc -> Int

.file : SrcLoc -> String

.line : SrcLoc -> Int

Hint: 

Show SrcLoc

.file : SrcLoc -> String

Visibility: public export

file : SrcLoc -> String

Visibility: public export

.line : SrcLoc -> Int

Visibility: public export

line : SrcLoc -> Int

Visibility: public export

.col : SrcLoc -> Int

Visibility: public export

col : SrcLoc -> Int

Visibility: public export

fcToSrcLoc : FC -> SrcLoc

  Convert an Idris 2 FC to a SrcLoc.

Visibility: export