module

/-! Module docstring -/

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

/-- A theorem. -/
theorem t : f = f := rfl
