import Mathlib.Tactic def hello := "world" -- Thank Grant for setting this up.