From 9fdaefe5391535d6436886051cc620986d10a081 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 10 Jul 2025 15:30:46 -0700 Subject: [PATCH] doc: Cleanup tactic documentation --- Pantograph/Protocol.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 086fe92..a003e8d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -257,13 +257,16 @@ structure GoalTactic where autoResume?: Option Bool := .none -- One of the fields here must be filled 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 have?: Option String := .none let?: 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 deriving Lean.FromJson