0.2.19

New Issue

feat: Add extraction of sorrys from compilation steps
chore: Remove most catalog filters in Environment.lean. A FFI user should implement these as they see fit.
fix: Tactics should produce .syntheticOpaque goals
chore: Bump Lean version to v4.12.0
fix: Delayed MVar translation in MetaTranslate

2024-10-09

100% Completed

feat: Capture environment in drafting

#113 by aniva was merged 2024-10-12 16:59:41 -07:00

frontend/environment

feat: Enable environment capture during frontend.process

part/Environment

#112 by aniva was closed 2024-10-12 16:59:33 -07:00

chore: Update Lean to v4.12.0

#108 by aniva was merged 2024-10-08 09:49:09 -07:00

feat: Remove most filters on catalog

part/Environment

#105 by aniva was merged 2024-10-06 16:12:23 -07:00

fix: Tactics should produce .syntheticOpaque goals

#100 by aniva was merged 2024-10-03 08:47:31 -07:00

feat: Expose GoalState functions

#94 by aniva was merged 2024-09-08 12:10:47 -07:00

Refactor out the Pantograph executable and lib into different targets

#93 by aniva was closed 2024-09-08 13:40:12 -07:00 goal/automatic