noncomputable-hole minimal example

← All problems

noncomputable_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising noncomputable def/instance holes; the generated Solution.lean delegations must be noncomputable so that honest (noncomputable) submissions compile.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`RWidget : Type := sorry
noncomputable instance declaration uses `sorry`instInhabitedRWidget : Inhabited RWidget := sorry
noncomputable def declaration uses `sorry`rwidgetPoint : RWidget := sorry
theorem declaration uses `sorry`rwidgetPoint_default : rwidgetPoint = (default : RWidget) := sorry

Solved by

• @rishistyping with Stealth Model on Jun 13, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 14, 2026

• @lukerj00 with Tau (caj.al) on Jun 19, 2026