Game/Metadata.lean

import GameServer.Commands

import Game.MyNat.Definition

import Game.Doc.Definitions
import Game.Doc.Tactics

import Game.Tactic.FromMathlib

import Game.Tactic.Induction
import Game.Tactic.Cases
import Game.Tactic.Rfl
import Game.Tactic.Rw
import Game.Tactic.Use
import Game.Tactic.Ne
import Game.Tactic.Xyzzy
import Game.Tactic.SimpAdd
-- import Std.Tactic.RCases
-- import Game.Tactic.Have
-- import Game.Tactic.LeftRight
big refactor 2023-05-15 15:05:02 +02:00			`import GameServer.Commands`

			`import Game.MyNat.Definition`

			`import Game.Doc.Definitions`
			`import Game.Doc.Tactics`

do not import all of mathlib 2024-03-14 10:38:03 +01:00			`import Game.Tactic.FromMathlib`
import Mathlib.Tactic everywhere 2023-08-04 17:14:49 +02:00
big refactor 2023-05-15 15:05:02 +02:00			`import Game.Tactic.Induction`
the tactic of tactics 2023-10-15 03:17:30 +02:00			`import Game.Tactic.Cases`
big refactor 2023-05-15 15:05:02 +02:00			`import Game.Tactic.Rfl`
			`import Game.Tactic.Rw`
custom use tactic 2023-10-28 11:17:20 +02:00			`import Game.Tactic.Use`
pretty-printer for not equal 2023-10-28 22:00:41 +02:00			`import Game.Tactic.Ne`
add mystical ancient tactic 2023-10-23 13:43:48 +01:00			`import Game.Tactic.Xyzzy`
make simp_add available in the entire game #54 2024-03-18 16:21:38 +01:00			`import Game.Tactic.SimpAdd`
import Mathlib.Tactic everywhere 2023-08-04 17:14:49 +02:00			`-- import Std.Tactic.RCases`
			`-- import Game.Tactic.Have`
			`-- import Game.Tactic.LeftRight`