2024-11-22T20:57:37Z - 2025-02-22T20:57:37Z
Overview
5 Releases published by 1 user
Published
v0.2.25
Published
v0.2.24
Published
v0.2.23
Published
v0.2.22
Published
v0.2.21
28 Pull requests merged by 1 user
Merged
#166 fix: Use in-context environment in sorry collection
Merged
#165 doc: Manual about env.{describe,module_read}
Merged
#164 chore: Code cleanup
Merged
#161 fix: Panic in exprProjToApp
Merged
#159 feat: Module reading functions
Merged
#157 feat: Pickle constants in goal state
Merged
#158 feat: Draft tactic REPL interface
Merged
#156 chore: Update version to 0.2.25
Merged
#134 chore: Update Lean to v4.15.0
Merged
#153 feat: Draft tactic
Merged
#155 chore: Update version
Merged
#152 fix: Incorrect binder capture
Merged
#154 feat: Add source location extraction
Merged
#149 feat: Simplify sexp printing
Merged
#148 fix: Unnecessary instantiation call
Merged
#141 feat: Print value of arbitrary mvar and goals in goal state
Merged
#145 doc: Add limitations
Merged
#146 chore: Update version
Merged
#144 fix: Reset core message log
Merged
#128 feat: Extract type error and new constants
Merged
#139 fix: Tactic failure on synthesizing placeholder
Merged
#143 chore: Add aarch64 build targets to flake
Merged
#140 chore: Update version
Merged
#135 fix: Capture nested tactic failure
Merged
#123 doc: Design Rationale Document
Merged
#133 doc: Documentation cleanup and update
Merged
#129 feat: Pickling goal states
Merged
#130 feat: Erase macro scopes in sexp
1 Pull request proposed by 1 user
Proposed
#136 chore: Version 0.3
14 Issues closed from 1 user
Closed
#162 Take generated constants into account
Closed
#163 Clean up code
Closed
#142 Pickle new constants generated in proof state
Closed
#160 Projection conversion function panics
Closed
#127 Drafting tactic in goals
Closed
#150 Allow LSP-like behaviour of finding definition location via symbol
Closed
#131 Add aarch64-{linux,darwin} targets in flake
Closed
#138 Articulation of Finished Proof
Closed
#126 Extraction of new symbols in each compilation unit
Closed
#125 Wrong code/Compilation Failure Extraction
Closed
#122 Mathlib4 Parsing Error
Closed
#114 Incremental and intercepted parsing of Lean code
Closed
#124 Erase macro scopes in sexp binders
Closed
#95 Pickling
5 Issues created by 1 user
Opened
#132 Proof state merger
Opened
#137 Pickle environment extensions
Opened
#147 Move Tactics to a Standalone Library
Opened
#151 Add unsafe detection in goal.print
Opened
#167 Allow alternative environment initiation
1 Unresolved Conversation
Open
#102
Timeout for tactics