Package-level declarations

Types

Link copied to clipboard

The identifiers a theory gives its clauses in comments: a clause followed, on the line of its full stop, by a comment of a single word (h :- b. % r5, the clause spanning one line or more) is tagged with it (RULE). Under prologStrictCompatibility a clause so tagged is the defeasible rule or premise of that identifier, the others strict rules and axioms; otherwise the tag changes nothing. The comments are read with the lexer of 2P-Kt, which keeps them, and the clauses are those its parser gives.