-
Notifications
You must be signed in to change notification settings - Fork 67
CJ Bell edited this page Oct 8, 2016
·
1 revision
Sentences: each command sent to CoqTop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF). Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity." In practice, the command sentences sent to CoqTop are terminated at the "." and start with any previous whitespace. Each sentence is assigned a unique stateId after being sent to Coq (via Add). States:
- Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing)
- Processed:
- InProgress:
- Incomplete: the validity of the sentence cannot be checked due to a prior error
- Complete:
- Error: the sentence has an error error
State ID 0 is reserved as 'null' or 'default' state. (The 'query' command suggests that it might also refer to the currently-focused state, but I have not tested this yet). The first command should be added to state ID 0. Queries are typically performed w.r.t. state ID 0.