Idris2Doc : Protocol.IDE.FileContext

Protocol.IDE.FileContext

(source)
Reexports
import public Libraries.Text.Bounded
Definitions
record FileContext : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFileContext : String -> Bounds -> FileContext

  Projections:
  
.file : FileContext -> String
  
.range : FileContext -> Bounds

  Hints:
  
Cast (FileName, NonEmptyFC) FileContext
  
FromSExpable FileContext
  
SExpable FileContext
.file : FileContext -> String
  Totality: total
  Visibility: public export
file : FileContext -> String
  Totality: total
  Visibility: public export
.range : FileContext -> Bounds
  Totality: total
  Visibility: public export
range : FileContext -> Bounds
  Totality: total
  Visibility: public export