The prove
command verifies a sentence and stores it as a verified sentence value <sentencevalue>
into a sentence variable <sentencevariable>
.
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 <scopes>
.
The sentence [sentence]
may depend on the bound predicates <predicates>
specified in the predicate list. If the code in the scope successfully executes, this sentence is stored as a verified sentence value <sentencevalue>
into the sentence variable <sentencevariable>
[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:
assume <assume> not <not> given <given> choose <choose>