Numbered sorry capture #278

New issue

Open

opened 2025-08-14 12:30:48 -07:00 by aniva · 0 comments

aniva commented

2025-08-14 12:30:48 -07:00

Owner

Currently for drafting and search target distillation, we don't have information about the syntactic position of each captured sorry.

After parsing, we can replace each term-level sorry with one that has a unique tag. Then we can use this tag to associate goals with sorrys. If there are goals that have the same tag, it is an indication that articulation might not be possible.

Currently for drafting and search target distillation, we don't have information about the syntactic position of each captured `sorry`. After parsing, we can replace each term-level `sorry` with one that has a unique tag. Then we can use this tag to associate goals with `sorry`s. If there are goals that have the same tag, it is an indication that articulation might not be possible.