instance-hole minimal example

← All problems

instance_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising instance + theorem holes; instances must be named so the comparator can address them.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`WidgetCarrier : Type := sorry
instance declaration uses `sorry`instInhabitedWidget : Inhabited WidgetCarrier := sorry

Solved by

Not yet solved.