lean2/tests/lean/local_notation_bug.lean.expected.out