Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proofs should track the current goal #12

Open
leotrs opened this issue Feb 19, 2022 · 1 comment
Open

Proofs should track the current goal #12

leotrs opened this issue Feb 19, 2022 · 1 comment

Comments

@leotrs
Copy link
Owner

leotrs commented Feb 19, 2022

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.

@leotrs
Copy link
Owner Author

leotrs commented Feb 22, 2022

This is currently implemented with the exception of steps that change the goal.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant