- feat(frontend): [Experimental]
frontend.refactor
Refactoring feature for preparing the start state of a proof search
- feat(repl):
env.parse
, Running a parser until it finishes and reports the finished position
- feat(goal): Use
tacticSeq
parser.
- fix(goal): Erase
MessageData
from synthetic mvars to prevent compacting closures
- fix(frontend): Capture local instances in sorrys
#258
by aniva was merged 2025-07-30 21:56:06 -07:00
#257
by aniva was merged 2025-07-30 12:37:01 -07:00
#254
by aniva was merged 2025-07-29 11:49:19 -07:00
#253
by aniva was merged 2025-07-28 16:06:18 -07:00
#252
by aniva was merged 2025-07-28 16:05:08 -07:00
#251
by aniva was merged 2025-07-25 15:53:37 -07:00
#250
by aniva was closed 2025-07-25 15:53:37 -07:00
#246
by aniva was merged 2025-07-22 12:52:06 -07:00
#245
by aniva was merged 2025-07-18 15:12:31 -07:00
#244
by aniva was merged 2025-07-13 23:14:57 -07:00
#242
by aniva was merged 2025-07-13 23:03:14 -07:00
#241
by aniva was closed 2025-07-13 23:03:14 -07:00
#240
by aniva was merged 2025-07-13 23:00:22 -07:00
#239
by aniva was closed 2025-07-13 23:02:21 -07:00
#238
by aniva was closed 2025-07-13 23:16:15 -07:00
#237
by aniva was merged 2025-07-12 12:09:33 -07:00
#234
by aniva was merged 2025-07-22 09:19:41 -07:00