Used constant for tactic info extraction #118

Closed
opened 2024-11-03 12:16:16 -08:00 by aniva · 1 comment
Owner
https://github.com/leanprover-community/repl/pull/59
aniva added this to the 0.2.20 milestone 2024-11-03 12:16:17 -08:00
aniva added the
category
feature
label 2024-11-03 12:16:17 -08:00
aniva self-assigned this 2024-11-03 12:16:17 -08:00
aniva added a new dependency 2024-11-05 14:40:28 -08:00
Author
Owner
#119
aniva closed this issue 2024-11-13 17:01:06 -08:00
Sign in to join this conversation.
No Milestone
No project
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Reference: aniva/Pantograph#118
No description provided.