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

[sonmarcho]

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.