feat: Collect holes in Lean file and put them into a `GoalState` #99

Merged

aniva merged 14 commits from frontend/collect-holes into dev

2024-10-03 15:43:01 -07:00

Author	SHA1	Message	Date
Leni Aniva	10cb32e03f	Merge branch 'dev' into frontend/collect-holes	2024-10-03 11:47:38 -07:00
Leni Aniva	a03eeddc9b	fix: Variable duplication in nested translation	2024-10-03 11:46:09 -07:00
Leni Aniva	530a1a1a97	fix: Extracting `sorry`s from coupled goals	2024-10-03 11:35:54 -07:00
Leni Aniva	143cd289bb	fix: Extraction of sorry's from nested tactics	2024-10-03 01:29:46 -07:00
Leni Aniva	18cd1d0388	fix: Extracting sorrys from sketches	2024-10-02 22:22:20 -07:00
Leni Aniva	bec84f857b	fix: repl build failure	2024-09-09 18:43:34 -07:00
Leni Aniva	fe8b259e4f	feat: Set root when there's just one mvar	2024-09-09 17:37:59 -07:00
Leni Aniva	f729a357b9	Merge branch 'dev' into frontend/collect-holes	2024-09-09 17:35:10 -07:00
Leni Aniva	9f0de0957e	doc: Update documentation for frontend command	2024-09-09 12:39:32 -07:00
Leni Aniva	762a139e78	feat: Export frontend functions	2024-09-09 12:30:32 -07:00
Leni Aniva	4f5950ed78	feat: Convert holes to goals	2024-09-09 12:26:46 -07:00
Leni Aniva	08fb53c020	test: Frontend process testing	2024-09-09 10:18:20 -07:00
Leni Aniva	8e3241c02a	refactor: Move all frontend functions to `Frontend`	2024-09-08 15:02:43 -07:00
Leni Aniva	860344f9c5	refactor: Factor out `FrontendM` driver	2024-09-08 13:44:46 -07:00