Tptp.Resolver.None (Tptp v0.1.0)

Copy Markdown View Source

Records an include and does not follow it.

The right resolver when the include graph is somebody else's problem: a prover handed the file will resolve its own includes, and reading them here would be work done twice and a chance to disagree about what Axioms/SET007+0.ax means.

Declining is not a failure, so no diagnostic is raised. Tptp.Unit still records the directive, so Tptp.File.includes/1 reports what was skipped.