lean2/tests/lean/bad_id.lean