We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6ceee8e commit 9ac6ae4Copy full SHA for 9ac6ae4
REPL/Main.lean
@@ -205,6 +205,8 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
205
let tactics ← match s.allTactics with
206
| some true => tactics trees
207
| _ => pure []
208
+ -- The list is repeated, so we only keep the second half.
209
+ let tactics := tactics.drop (tactics.length / 2)
210
let cmdSnapshot :=
211
{ cmdState
212
cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
0 commit comments