lean4-htt/tests/lean/bad_error5.lean.expected.out

1 line
88 B
Text

bad_error5.lean:13:10: error: code generation failed, VM does not have code for 'sorry'