Incremental and intercepted parsing of Lean code #114
Labels
No Label
category
bug
category
doc
category
feature
category
optimization
category
organization
part/Delation
part/Elab
part/Environment
part/FFI
part/Frontend
part/Goal
part/REPL
part/Serial
priority
high
priority
irrelevant
priority
low
priority
medium
No Milestone
No project
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Depends on
#113 feat: Capture environment in drafting
aniva/Pantograph
Reference: aniva/Pantograph#114
Loading…
Reference in New Issue
No description provided.
Delete Branch "%!s(<nil>)"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The Putnam dataset has this:
Suppose the
abbrev
line is commented out, it would be a useful feature to parse the theorem only and skip over the abbrev. Specifically we could let the user decide the fate of each compilation unit and give the user the choice to update the environment or not.Partly solved by #113