# `Tptp.Lint.Rules.DefinedWord`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/lint/rules/defined_word.ex#L1)

A `$`-word outside the vocabularies named by the `:==` conditions.

The `$` prefix is reserved to the TPTP language, so `$wibble` is not a symbol a
problem may introduce. `$$wibble` is the system-specific form and is not checked.
The vocabularies come from `Tptp.Bnf.Vocabulary`, generated from the same BNF as
the grammar, so the two cannot diverge.

A warning rather than an error: an unrecognised `$`-word is usually a
misspelling, but a prover extension not yet incorporated into the BNF is also
possible.

## Coverage over the TPTP library

This rule reports nothing on TPTP v9.3.1, and reported 76 occurrences across five
modal system names under the BNF up to v9.3.1.2, whose `<ntf_modal_system>` named
six systems and `<ntf_modal_axiom>` six axioms where the Non-classical Logics
section of the TPTP language page stated sixteen and ten. v9.3.1.3 completed both
lists, and their `$`-words reach this rule through `<reserved_word>`, which is
what it consults.

---

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