aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
Conversation 0 Commits 22 Files Changed 9 +6 -1
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit db35ec7187 - Show all commits

7
README.md
View File

@ -81,7 +81,12 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
- `options.print`: Display the current set of options - `options.print`: Display the current set of options
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal - `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr":
<expr>]}`: Execute a tactic string on a given goal. `tactic` executes an
ordinary tactic, `expr` assigns an expression to the current goal, `have`
executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step
of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic
mode.
- `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state - `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals. - `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
- `goal.print {"stateId": <id>}"`: Print a goal state - `goal.print {"stateId": <id>}"`: Print a goal state