def foo (x : Nat) : Nat := sorry

def bar := sorry

#eval 1

#check Nat

--^ collectDiagnostics
--^ interactiveDiagnostics