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

Not yet solved.