module

/-! Module docstring -/

/-- A definition. -/
def f := 1

/-- A theorem. -/
theorem t : f = 1 := sorry

theorem trfl : f = 1 := rfl