Idris2Doc : Text.TOML.Parser

Text.TOML.Parser

(source)
Definitions
data ElemType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Table : TableType -> ElemType
  
Array : ArrayType -> ElemType
0 ParentType : ElemType -> Type
  Totality: total
  Visibility: public export
record PathElem : Type
  Key together with the a value and its type encountered in a
  TOML tree.

  Totality: total
  Visibility: public export
  Constructor: 
PE : (tpe : ElemType) -> ParentType tpe -> KeyToken -> PathElem

  Projections:
  
.key : PathElem -> KeyToken
  
.parent : ({rec:0} : PathElem) -> ParentType (tpe {rec:0})
  
.tpe : PathElem -> ElemType
.tpe : PathElem -> ElemType
  Totality: total
  Visibility: public export
tpe : PathElem -> ElemType
  Totality: total
  Visibility: public export
.parent : ({rec:0} : PathElem) -> ParentType (tpe {rec:0})
  Totality: total
  Visibility: public export
parent : ({rec:0} : PathElem) -> ParentType (tpe {rec:0})
  Totality: total
  Visibility: public export
.key : PathElem -> KeyToken
  Totality: total
  Visibility: public export
key : PathElem -> KeyToken
  Totality: total
  Visibility: public export
record TOMLView : Type
  Totality: total
  Visibility: public export
  Constructor: 
TV : SnocList PathElem -> Maybe TomlValue -> TOMLView

  Projections:
  
.cur : TOMLView -> Maybe TomlValue
  
.path : TOMLView -> SnocList PathElem
.path : TOMLView -> SnocList PathElem
  Totality: total
  Visibility: public export
path : TOMLView -> SnocList PathElem
  Totality: total
  Visibility: public export
.cur : TOMLView -> Maybe TomlValue
  Totality: total
  Visibility: public export
cur : TOMLView -> Maybe TomlValue
  Totality: total
  Visibility: public export
pth : SnocList PathElem -> List KeyToken -> Maybe TomlValue -> Either (Bounded TomlErr) TOMLView
  Totality: total
  Visibility: public export
tableAt : List1 KeyToken -> TomlValue -> Either (Bounded TomlErr) (SnocList PathElem, TomlValue)
  Totality: total
  Visibility: public export
arrayAt : List1 KeyToken -> TomlValue -> Either (Bounded TomlErr) (SnocList PathElem, SnocList TomlValue)
  Totality: total
  Visibility: public export
tryInsert : List1 KeyToken -> TomlValue -> TomlValue -> Either (Bounded TomlErr) TomlValue
  Totality: total
  Visibility: public export
data TomlItem : Type
  Totality: total
  Visibility: public export
  Constructors:
  
TableName : List1 KeyToken -> TomlItem
  
ArrayName : List1 KeyToken -> TomlItem
  
KeyVal : List1 KeyToken -> TomlValue -> TomlItem
parse : Origin -> String -> Either (ParseError TomlParseError) TomlValue
  Totality: total
  Visibility: export