You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The statement of a theorem-like should always include a claim. The claim becomes the goal of the corresponding proof. Each step's handrail should include a new button, "show goal", that would display (or highlight, if within viewport) the claim that is the current goal. For this purpose, rsm-make will have to keep track of what is the current goal. Steps can change the goal, and sub-steps generally have a goal that is a claim on their parent step, while top-level steps have a goal that is the goal of the entire proof.
The text was updated successfully, but these errors were encountered:
The statement of a theorem-like should always include a claim. The claim becomes the goal of the corresponding proof. Each step's handrail should include a new button, "show goal", that would display (or highlight, if within viewport) the claim that is the current goal. For this purpose, rsm-make will have to keep track of what is the current goal. Steps can change the goal, and sub-steps generally have a goal that is a claim on their parent step, while top-level steps have a goal that is the goal of the entire proof.
The text was updated successfully, but these errors were encountered: