Parse and enter environment at arbitrary points of the input #97

New Issue

aniva · 2024-09-08T01:09:59-07:00

aniva commented

2024-09-08 01:09:59 -07:00

When processing e.g. the miniF2F dataset, our users need to parse Lean expressions of the form

theorem example_123 (a: Nat), Property a := sorry

It would be helpful to capture the CommandElabM or TermElabM monadic state right before the point of the sorry. PyPantograph currently has an ad-hoc parser for this and it isn't very reliable.

When processing e.g. the miniF2F dataset, our users need to parse Lean expressions of the form ```lean theorem example_123 (a: Nat), Property a := sorry ``` It would be helpful to capture the `CommandElabM` or `TermElabM` monadic state right before the point of the `sorry`. PyPantograph currently has an ad-hoc parser for this and it isn't very reliable.

aniva added this to the 0.3 milestone 2024-09-08 01:09:59 -07:00

aniva added the

category

feature

part/Elab

labels 2024-09-08 01:09:59 -07:00

aniva self-assigned this 2024-09-08 01:09:59 -07:00

aniva added the

part/Frontend

label 2024-09-08 13:39:54 -07:00

aniva modified the milestone from 0.3 to TACAS '25

2024-09-08 13:48:50 -07:00