src/repl.lean (1 line):
	- line 367: -- TODO: refactor so that finalizing a proof is a separate top-level call