prove

The prove command verifies a sentence and stores it as a verified sentence value into a sentence variable.

Syntax

prove [identifier]: [sentence]{
        ...
}
prove [identifier][[predicate0](num_args), [predicate1], ...]: [sentence]{
        ...
}

The prove command begins with the keyword prove followed by a variable identifier. Optionally, a list of predicate identifiers may be present. The list begins with the [ character, and ends with the ] character. Each entry in the list is a predicate identifier, followed by an optional number of arguments. If present, the number of arguments is denoted by the ( character, a non-negative integer, and the ) character. Entries in the predicate list are separated with the , character.

Following the variable identifier and optional predicate identifiers is the : character and a sentence. The command is terminated with a new scope.

Behavior

The sentence [sentence] may depend on the bound predicates specified in the predicate list. If the code in the scope successfully executes, this sentence is stored as a verified sentence value into the sentence variable [identifier].

The execution of the code inside of the new scope depends on sentence specified by [sentence]. This sentence is called the goal of the scope.

The following commands only run in a scope with a goal: