Jon Eugster 3a3471c615 throw error in regular difficulty if tactic not unlocked

2023-10-09 11:23:37 +02:00

..

AbstractCtx.lean

satisfy unused variable linter

2023-09-01 12:11:49 +02:00

Commands.lean

hide hidden items everywhere

2023-10-03 10:17:16 +02:00

EnvExtensions.lean

Add NewHiddenTactic command

2023-10-02 12:50:19 +02:00

FileWorker.lean

throw error in regular difficulty if tactic not unlocked

2023-10-09 11:23:37 +02:00

Game.lean

throw error in regular difficulty if tactic not unlocked

2023-10-09 11:23:37 +02:00

Graph.lean

remove path command

2023-07-11 13:46:15 +02:00

InteractiveGoal.lean

…

RpcHandlers.lean

…

TacticDocstringTest.lean

add Template server-side

2023-08-25 18:04:10 +02:00

Watchdog.lean

throw error in regular difficulty if tactic not unlocked

2023-10-09 11:23:37 +02:00