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

Documentation for print_goal_consts and print_goal_depth is swapped in the SAW manual. #789

Closed
ChrisEPhifer opened this issue Jul 21, 2020 · 0 comments · Fixed by #790
Closed
Assignees
Labels
documentation Issues involving documentation type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@ChrisEPhifer
Copy link
Member

The SAW manual has the following under the heading "Proof Script Diagnostics":

During development of a proof, it can be useful to print various information about the current goal. The following tactics are useful in that context.

  • print_goal : ProofScript () prints the entire goal in SAWCore syntax.
  • print_goal_consts : ProofScript () takes an integer argument, n, and prints the goal up to depth n. Any elided subterms are printed with a ... notation.
  • print_goal_depth : Int -> ProofScript () prints a list of the names of subterms that are folded in the current goal.
  • print_goal_size : ProofScript () prints the number of nodes in the DAG representation of the goal.

While the types are correct, the descriptions of print_goal_consts and print_goal_depth appear to be reversed; additionally, the description of print_goal_consts (currently appearing as the description of proof_goal_depth) does not make it clear that it will display the unfoldable constants in the current goal.

@ChrisEPhifer ChrisEPhifer added type: bug Issues reporting bugs or unexpected/unwanted behavior documentation Issues involving documentation labels Jul 21, 2020
@ChrisEPhifer ChrisEPhifer self-assigned this Jul 21, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Issues involving documentation type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant