From dc6e79def7a00e1d4a2e936a09e578c851b45bc4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 11 Apr 2024 16:18:04 -0700 Subject: [PATCH] doc: Update error message in interaction --- Pantograph.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Pantograph.lean b/Pantograph.lean index a0580d2..f59bc11 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -129,7 +129,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure ( Except.ok (← goalConv goalState args.goalId)) | .none, .none, .none, .none, .some false => do pure ( Except.ok (← goalConvExit goalState)) - | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied") + | _, _, _, _, _ => pure (Except.error <| + errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied") match nextGoalState? with | .error error => return .error error | .ok (.success nextGoalState) =>