Data.String.Builder

Definitions

record Builder : Type -> Type

  A simple mutable string builder based on a snoc list wrapped
  in a mutable reference.

Totality: total
Visibility: export
Constructor: 

B : Ref q (SnocList String) -> Builder q

Projection: 

.ref : Builder q -> Ref q (SnocList String)

builder : F1 q (Builder q)

  Creates a new string builder.

Totality: total
Visibility: export

withBuilder : (Builder q => F1' q) -> String

  Creates a string from a string building function.

Totality: total
Visibility: export

linebreak : Builder q => F1' q

  Append a linebreak to the string builder.

Totality: total
Visibility: export

tab : Builder q => F1' q

  Append a single tab to the string builder.

Totality: total
Visibility: export

space : Builder q => F1' q

  Append a single space to the string builder.

Totality: total
Visibility: export

spaces : Builder q => Nat -> F1' q

  Append the given number of spaces to the string builder.

Totality: total
Visibility: export

putText : Builder q => String -> F1' q

  Append the given string to the string builder.

Totality: total
Visibility: export

putTextLn : Builder q => String -> F1' q

  Append the given string followed by a carriage return
  to the string builder.

Totality: total
Visibility: export

putTextSep : Builder q => String -> F1' q

  Append the given string followed by a space character return
  to the string builder.

Totality: total
Visibility: export

putChars : Builder q => List Char -> F1' q

  Appends the given list of characters to the string builder.

Totality: total
Visibility: export

putCharsLn : Builder q => List Char -> F1' q

  Append the given list of characters followed by a carriage return
  to the string builder.

Totality: total
Visibility: export

putShow : Builder q => Show a => a -> F1' q

  Show a value and append it to the string builder.

Totality: total
Visibility: export

putShowLn : Builder q => Show a => a -> F1' q

  Show a value and append it to the string builder followed
  by a carriage return.

Totality: total
Visibility: export

putShowSep : Builder q => Show a => a -> F1' q

  Show a value and append it to the string builder followed
  by a space character.

Totality: total
Visibility: export

putVal : Builder q => Interpolation a => a -> F1' q

  Interpolate a value and append it to the string builder.

Totality: total
Visibility: export

putValLn : Builder q => Interpolation a => a -> F1' q

  Interpolate a value and append it to the string builder followed
  by a carriage return.

Totality: total
Visibility: export

putValSep : Builder q => Interpolation a => a -> F1' q

  Interpolate a value and append it to the string builder followed
  by a space character.

Totality: total
Visibility: export

putAll : Builder q => List String -> F1' q

  Append a list of strings to the string builder.

Totality: total
Visibility: export

putLeftPadded : Builder q => Nat -> Char -> String -> F1' q

  Append a string, padding it on the left with the given character.

Totality: total
Visibility: export

padRightPadded : Builder q => Nat -> Char -> String -> F1' q

  Append a string, padding it on the right with the given character.

Totality: total
Visibility: export