def-hole minimal example

← All problems

def_hole_example

Submitter: Kim Morrison.

Notes: Minimal example exercising def + theorem holes through the comparator def-hole pipeline.

Source: Unavailable.

Informal solution: Unavailable.

def declaration uses `sorry`foo : Nat := sorry
theorem declaration uses `sorry`foo_def : foo = 37 := sorry

Solved by

Not yet solved.