# `Tptp.Statement.Annotated`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/statement/annotated.ex#L1)

An annotated formula: `fof(name, role, formula, source, info).`

## Retention of `source` and `info`

These fields constitute the TSTP. A derivation is a set of annotated formulae
whose `source` records the inference producing each one and the parents it was
derived from, so a reader discarding them can read problems but not proofs. They
are already parsed, the grammar covering `<source>` and `<useful_info>` in full,
so retaining them allows proof reconstruction to be a traversal rather than a
second parse.

## Uninterpreted fields

`role` is the node as parsed rather than an atom from a closed set:
`<formula_role>` is a `<lower_word>` in the `::=` grammar and is restricted to
the named set only by the `:==` conditions, so rejecting an unrecognised role is
a lint decision rather than a parse decision. Likewise `formula` is the
unelaborated subtree; in a THF statement it may be a type, a term or a formula,
and the grammar does not distinguish them.

# `t`

```elixir
@type t() :: %Tptp.Statement.Annotated{
  formula: Tptp.Node.t(),
  info: Tptp.Node.t() | nil,
  language: :thf | :tff | :tcf | :fof | :cnf | :tpi,
  len: non_neg_integer(),
  name: Tptp.Node.t(),
  off: non_neg_integer(),
  role: Tptp.Node.t(),
  source: Tptp.Node.t() | nil
}
```

One annotated formula, with its four grammatical slots kept apart as separate subtrees.

---

*Consult [api-reference.md](api-reference.md) for complete listing*