Pantograph/Pantograph.lean

import Pantograph.Compile
import Pantograph.Condensed
import Pantograph.Environment
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Pantograph.Serial
import Pantograph.Version
feat: Basic tactic extraction (before/after/tactic) 2024-05-28 17:25:22 -07:00			`import Pantograph.Compile`
refactor: Use `MVarId` across the board 2024-09-06 21:07:12 -07:00			`import Pantograph.Condensed`
feat: Basic tactic extraction (before/after/tactic) 2024-05-28 17:25:22 -07:00			`import Pantograph.Environment`
Rename tactic to goal and restructure 2023-10-15 12:31:22 -07:00			`import Pantograph.Goal`
feat: Basic tactic extraction (before/after/tactic) 2024-05-28 17:25:22 -07:00			`import Pantograph.Library`
Store states instead of goals 1. Rename {Commands, Protocol}, and {Symbols, Symbol} 2. Store the root mvarId in the proof state along with goal indices 3. Add diagnostics function which prints out the state 4. Bump version to 0.2.6 (breaking change) Documentations pending 2023-10-15 17:15:23 -07:00			`import Pantograph.Protocol`
			`import Pantograph.Serial`
refactor: Refactor REPL out of main library fix: Calc previous rhs not found bug 2024-09-06 22:01:36 -07:00			`import Pantograph.Version`