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 v0.2.20 milestone 2024-11-03 12:16:17 -08:00
aniva self-assigned this 2024-11-03 12:16:17 -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 participant
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.