import Mathlib def hello := "world" #print "hi"