Alexander Bentkamp 97dc648452 use goal lctx for hints ...

Closes  #135

2023-11-30 20:38:25 +01:00

..

AbstractCtx.lean

Turn some logInfo into trace[debug] to toggle the off for building

2023-10-17 16:01:39 +02:00

Commands.lean

json api

2023-11-30 10:51:03 +01:00

EnvExtensions.lean

json api

2023-11-30 10:51:03 +01:00

FileWorker.lean

loading progress

2023-11-28 11:43:32 +01:00

Game.lean

json api

2023-11-30 10:51:03 +01:00

Graph.lean

remove path command

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

ImportModules.lean

also display loading of constants

2023-11-28 14:53:05 +01:00

InteractiveGoal.lean

change folder structure

2023-04-26 01:31:35 +02:00

RpcHandlers.lean

use goal lctx for hints

2023-11-30 20:38:25 +01:00

Utils.lean

add file

2023-10-18 14:49:30 +02:00

Watchdog.lean

fixes of lean bump

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