- Load/check file:
C-c C-l. - Show goals:
C-c C-?. - Accept goal value:
C-c C-SPACE - forward goal:
C-c C-f - backward goal:
C-c C-b - Normal form:
C-c C-n - see how to write symbol:
M-x quail-show-key. - Within goal: Case split:
C-c C-c. - Within goal: Refine:
C-c C-r. Partial give: makes new holes for missing arguments - Within goal: Type:
C-c C-t. - Within goal: Deduce type:
C-c C-d. - Within goal: Information:
C-c C-;.