Jon Eugster 8e3dfdea30 wip

2024-05-24 15:34:33 +02:00

..

Helpers

support translations of the games

2024-03-27 00:22:51 +01:00

Tactic

support translations of the games

2024-03-27 00:22:51 +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

turn defeq-hints on by default #45

2024-05-23 16:35:52 +02:00

EnvExtensions.lean

add 'using' as known keyword

2024-05-03 15:16:19 +02:00

FileWorker.lean

fix typo

2024-04-08 23:20:21 +02:00

Game.lean

remove watchdog

2023-12-15 22:17:09 +01:00

Graph.lean

remove watchdog

2023-12-15 22:17:09 +01:00

Helpers.lean

modify generated statement in inventory

2024-03-25 22:23:03 +01:00

Hints.lean

turn defeq-hints on by default #45

2024-05-23 16:35:52 +02:00

ImportModules.lean

also display loading of constants

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

InteractiveGoal.lean

fixes for v4.6.0-rc1

2024-02-29 10:34:24 +01:00

Inventory.lean

fix allowed keywords that are not tactics

2024-02-29 15:12:33 +01:00

Options.lean

cleanup; including using doc comment syntax for documentation like TacticDoc

2023-12-11 19:38:58 +01:00

RpcHandlers.lean

add defeq-hints #45

2024-05-23 16:33:55 +02:00

SaveData.lean

wip

2024-05-24 15:34:33 +02:00

Structures.lean

plug-in variables in hints client-side

2024-02-16 16:50:10 +01:00

Utils.lean

add file

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