Pantograph

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

feat: Extract used constants from invocation

category

feature

part/Frontend

#119 by aniva was merged 2024-11-10 21:29:35 -08:00

dev

frontend/data

0.2.20

feat: Capture environment in drafting

1

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

dev

frontend/environment

0.2.19

feat: Let tactic in REPL

category

feature

part/REPL

1

#111 by aniva was merged 2024-10-12 16:54:13 -07:00

dev

repl/tactic-let

TACAS '25

feat: Catch and print IO errors in REPL

#109 by aniva was merged 2024-10-08 23:50:37 -07:00

dev

repl/io-exception

TACAS '25

feat: Error reporting in frontend

#107 by aniva was merged 2024-10-05 22:39:24 -07:00

dev

frontend/error

TACAS '25

feat: Remove most filters on catalog

category

feature

part/Environment

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

dev

env/catalog

0.2.19

feat: Set automaticMode to true by default

category

feature

part/REPL

#101 by aniva was merged 2024-09-09 17:33:42 -07:00

dev

goal/automatic-mode

TACAS '25

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: Expose GoalState functions

category

feature

part/FFI

2

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

dev

lib/export

0.2.19

feat: Automatic Mode

1

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

dev

goal/automatic

TACAS '25

feat: Condensed interface

category

feature

part/Serial

#85 by aniva was merged 2024-08-15 22:41:59 -07:00

dev

serial/expr

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

feat: Handling of universe level names in elab

category

feature

part/Elab

#79 by aniva was closed 2024-06-23 13:33:55 -07:00

dev

parse/level

0.3

feat: Extraction of tactics from compiler

#76 by aniva was merged 2024-05-31 20:23:51 -07:00

dev

compile/tactic

TACAS '25

feat: Elementarized tactics with motives, congruence, and absurdity

6

#72 by aniva was merged 2024-06-12 13:52:46 -07:00

dev

goal/mapply

feat: Let tactic

category

feature

#70 by aniva was merged 2024-04-12 21:42:32 -07:00

dev

goal/let

0.3

feat: Option to collect dependent metavariables

category

feature

part/Goal

#69 by aniva was merged 2024-04-12 21:33:01 -07:00

dev

serial/goal

0.3

feat: Print precursor rules in env/inspect

#65 by aniva was merged 2024-04-11 15:35:15 -07:00

dev

env/inspect

0.3

feat: Add support for the have, conv, and calc tactics

category

feature

part/Goal

#59 by aniva was merged 2024-04-11 15:36:20 -07:00

dev

goal/have-conv-calc

0.3

Labels Milestones