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

doc: Cleanup tactic documentation

This commit is contained in:
Leni Aniva 2025-07-10 15:30:46 -07:00
parent bd7dde8235
commit 9fdaefe539
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Pantograph/Protocol.lean
View File

@ -257,13 +257,16 @@ structure GoalTactic where
autoResume?: Option Bool := .none autoResume?: Option Bool := .none
-- One of the fields here must be filled -- One of the fields here must be filled
tactic?: Option String := .none tactic?: Option String := .none
mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"} -- Changes the current category to {"tactic", "calc", "conv"}
mode?: Option String := .none
-- Assigns an expression to the current goal
expr?: Option String := .none expr?: Option String := .none
have?: Option String := .none have?: Option String := .none
let?: Option String := .none let?: Option String := .none
draft?: Option String := .none draft?: Option String := .none
-- In case of the `have` tactic, the new free variable name is provided here -- In case of the `have` and `let` tactics, the new free variable name is
-- provided here
binderName?: Option String := .none binderName?: Option String := .none
deriving Lean.FromJson deriving Lean.FromJson