0.2.25

New Issue

feat(goal): Draft tactic
fix(goal): Prohibit coupling in draft tactics and drafting
feat(serial): Pickle constants in goal state
feat(environment): Reading module and import data
chore: Update Lean to ~~v4.14.0~~ v4.15.0
fix(delate): Panic of projection normalization function

2025-01-30

100% Completed

fix: Use in-context environment in sorry collection

#166 by aniva was merged 2025-01-28 17:42:55 -08:00

bug/collect-sorry-generated-constants

doc: Manual about env.{describe,module_read}

part/Environment

#165 by aniva was merged 2025-01-26 22:04:29 -08:00

chore: Code cleanup

#164 by aniva was merged 2025-01-26 22:04:13 -08:00

Clean up code

#163 by aniva was closed 2025-01-26 22:04:51 -08:00

fix: Panic in exprProjToApp

#161 by aniva was merged 2025-01-24 15:05:05 -08:00

bug/expr-proj-to-app-panic

Projection conversion function panics

#160 by aniva was closed 2025-01-24 15:05:34 -08:00

feat: Module reading functions

part/Environment

#159 by aniva was merged 2025-01-24 15:01:17 -08:00

feat: Draft tactic REPL interface

#158 by aniva was merged 2025-01-16 10:32:48 -08:00

feat: Pickle constants in goal state

#157 by aniva was merged 2025-01-24 14:52:53 -08:00

chore: Update version to 0.2.25

#156 by aniva was merged 2025-01-13 12:29:12 -08:00

feat: Draft tactic

#153 by aniva was merged 2025-01-13 10:22:36 -08:00

goal/tactic-draft

Pickle new constants generated in proof state

#142 by aniva was closed 2025-01-24 15:05:54 -08:00

chore: Update Lean to v4.15.0

#134 by aniva was merged 2025-01-13 12:28:50 -08:00

Drafting tactic in goals

#127 by aniva was closed 2025-01-13 11:33:21 -08:00