Pantograph

feat: Tactic with timeout

1

#179 by aniva was merged 2025-03-28 21:31:59 -07:00

dev

repl/timeout

0.3

fix(goal): Name generation not available due to context

#174 by aniva was merged 2025-03-14 16:48:17 -07:00

dev

goal/tactic

0.3

chore: Cleanup the library system

#169 by aniva was merged 2025-03-08 21:19:01 -08:00

dev

chore/cleanup

0.3

feat: Draft tactic REPL interface

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

dev

tactic/draft

0.2.25

feat: Pickle constants in goal state

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

dev

serial/pickle

0.2.25

fix: Reset core message log

#144 by aniva was merged 2024-12-11 09:09:34 -08:00

dev

bug/core-state-error-linger

0.2.22

feat: Print value of arbitrary mvar and goals in goal state

#141 by aniva was merged 2024-12-11 16:52:20 -08:00

dev

goal/print

0.2.23

fix: Tactic failure on synthesizing placeholder

4

#139 by aniva was merged 2024-12-11 01:13:15 -08:00

dev

bug/tactic-failure-placeholder

0.2.22

fix: Capture nested tactic failure

1

#135 by aniva was merged 2024-12-07 18:51:26 -08:00

dev

bug/nested-tactic-failure

0.2.22

feat: Extract type error and new constants

1

#128 by aniva was merged 2024-12-11 01:25:36 -08:00

dev

frontend/infotree

0.2.22

doc: Design Rationale Document

category

doc

part/Goal

#123 by aniva was merged 2024-12-05 17:24:20 -08:00

dev

doc/rationale

0.3

feat: State and environment pickling

1

#120 by aniva was merged 2024-11-15 23:10:34 -08:00

dev

serial/pickle

0.2.21

fix: Delayed MVars in MetaTranslate

1

#110 by aniva was merged 2024-10-09 18:08:10 -07:00

dev

bug/frontend-translate-delayed-mvar

TACAS '25

fix: Tactics should produce .syntheticOpaque goals

1

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

dev

goal/tactic

0.2.19

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

5

#99 by aniva was merged 2024-10-03 15:43:01 -07:00

dev

frontend/collect-holes

TACAS '25

feat: Automatic Mode

1

#92 by aniva was merged 2024-09-08 12:25:07 -07:00

dev

goal/automatic

TACAS '25

fix: Instantiate type when detecting eq

#91 by aniva was merged 2024-09-03 19:19:10 -07:00

dev

bug/eq-detection-in-congruence

fix: Bindings in prograde tactics

#90 by aniva was merged 2024-09-03 18:15:58 -07:00

dev

bug/hidden-fvar-in-define

fix: Resume not taking type unification into account

1

#89 by aniva was closed 2024-09-02 19:43:36 -07:00

dev

bug/resume-type-unification

0.3

feat: Prograde tactics

category

feature

part/Goal

1

#83 by aniva was merged 2024-08-31 20:04:39 -07:00

dev

tactic/eval

0.3

Labels Milestones