0.3

New Issue

feat(env): Allow adding definitions/theorems to the environment
chore: Stabilize Lean to at least version 4.18.0
feat(goal): Add support for the have, conv, calc tactics
feat(frontend): Add proof scraping support
feat: Add ~~condensed~~ delated interface
feat(goal): Add automatic mode
feat(serial): Add environment/state pickling
doc: Add design rational documentation
feat(goal): Articulation of finished proof term (could be very ugly)
feat(goal): Tactic execution timeout

2025-04-01

100% Completed

Draft tactic hangs for some particular cases of have

#186 by aniva was closed 2025-04-09 00:21:52 -07:00

chore: Update Lean to v4.18.0

category

organization

#185 by aniva was merged 2025-04-08 10:59:54 -07:00

dev

chore/version

Remove CoreM library functions

category

chore

part/FFI

#184 by aniva was closed 2025-04-09 00:22:40 -07:00

fix: universe commands in environment capture

#183 by aniva was merged 2025-04-07 20:18:50 -07:00

dev

bug/variable-level-names-in-scope

fix: env.add Declarations with universe levels

#181 by aniva was merged 2025-03-29 15:48:13 -07:00

dev

bug/env-add-level

feat: Tactic with timeout

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

dev

repl/timeout

chore: Update Lean to v4.17.0, version to v0.3

category

organization

#178 by aniva was merged 2025-03-24 18:05:25 -07:00

dev

chore/version

feat: Update CoreM options from parsed header

#177 by aniva was merged 2025-03-28 18:56:22 -07:00

dev

frontend/env-init

feat(delate): Unfold matchers

category

feature

part/Delation

#176 by aniva was merged 2025-03-17 18:37:55 -07:00

dev

delate/instantiate

Add tracing tags in delation

category

feature

part/Delation

#175 by aniva was closed 2025-03-24 18:21:48 -07:00

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

feat(frontend): Alternative methods of initializing environment

category

feature

part/Frontend

#173 by aniva was merged 2025-03-14 16:48:40 -07:00

dev

frontend/env-init

GoalState.withContext should allow lifting

#171 by aniva was closed 2025-03-08 21:20:03 -08:00

chore: Cleanup the library system

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

dev

chore/cleanup

chore: Version bump

#168 by aniva was merged 2025-02-25 15:16:44 -08:00

dev

chore/version

Allow alternative environment initiation

#167 by aniva was closed 2025-03-28 19:08:09 -07:00

Take generated constants into account

#162 by aniva was closed 2025-01-31 13:16:42 -08:00

feat: Simplify sexp printing

category

feature

part/Delation

#149 by aniva was merged 2025-01-07 17:31:30 -08:00

dev

delate/sexp

fix: Unnecessary instantiation call

category

optimization

#148 by aniva was merged 2025-01-07 17:31:09 -08:00

dev

goal/tactic

Move Tactics to a Standalone Library

category

feature

part/Goal

#147 by aniva was closed 2025-03-08 21:20:16 -08:00

1 2 3