multi-hole-with-helpers regression example

← All problems

multi_hole_helpers_example

Submitter: Kim Morrison.

Notes: Regression test for trusted-helper support in multi-hole problems. Exercises three failure modes the generator used to have: (1) helpers at root namespace (`rootHelper`) must not get a spurious `open`; (2) the helper namespace `Helpers` differs from the module's last path component `MultiHoleHelpersExample`, so the injected `open` must be derived from the helper names rather than the module name; (3) the helper `Helpers.postHole` appears in source order *between* two holes, exercising the right-to-left edit pass against a layout where a sequential strip-then-replace pipeline (with helper ranges taken from `.ilean` and applied after hole-body replacement) would have shifted offsets. A submission that defines `Submission.Helpers.first := 1`, `Submission.Helpers.second_eq := rfl`, and `Submission.Helpers.third_eq := rfl` should be accepted.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`first : Nat := sorry
theorem declaration uses `sorry`second_eq : first + rootHelper + preHole = first + 141 := sorry
theorem declaration uses `sorry`third_eq : postHole = 1000 := sorry

Solved by

Not yet solved.