The use of opaque functions without `--split-files` generates files which don't typecheck in Lean

[sonmarcho]

trafficstars

Opaque functions are translated to axioms if we don't use --split-files, which can lead to issues because axioms are noncomputable in Lean, and all definitions using a non-computable definition should inherit the noncomputable attribute.