Idris2Doc : Text.Molfile.Parser.V2000

Text.Molfile.Parser.V2000

(source)
Definitions
v2000 : RExp True
  V2000 Counts line

  Totality: total
  Visibility: export
sdigits : Nat -> RExp True
  An arbitrary number of spaces and digits followed by a line break.

  Totality: total
  Visibility: export
smtExpr : RExp True
  Expression recognizing the remainder of an `SMT` entry in
  a v2000 properties block.

  Totality: total
  Visibility: export
styExpr : RExp True
  Expression recognizing the remainder of an `SYT` entry in
  a v2000 properties block.

  Totality: total
  Visibility: export
coordinatesV2 : RExp True
  Expression for V2000 coordinates.

  Totality: total
  Visibility: export
countsV2 : CSTCK q => ByteString -> F1 q CST
  Reads the number of atoms and bonds from a V2000 counts line,
  and sets up a new (mutable) graph accodringly.

  Totality: total
  Visibility: export
coordsV2 : CSTCK q => ByteString -> F1 q CST
  Converts a bytestring into a set of coordinates and
  writes it to the current atom.

  Totality: total
  Visibility: export
atomV2 : CSTCK q => F1 q CST
  Finalizes a V2000 atom, increasing the current node and
  moving to the bond block if all atoms have been processed.

  Totality: total
  Visibility: export
chargeV2 : CSTCK q => F1 q CST
  Sets an atom's charge and finalizes it via `atomV2`.

  Totality: total
  Visibility: export
bond : CSTCK q => F1 q CST
  Parses a V2000 bond entry and adds an edge to the graph.

  Totality: total
  Visibility: export
line : Nat -> a -> (CSTCK q => F1 q CST) -> (a, Step q CSz CSTCK)
  Totality: total
  Visibility: export
prop2 : Steps q CSz CSTCK
  Totality: total
  Visibility: export