lean4-htt/tests/lean/490.lean.expected.out
2022-01-26 19:15:45 -08:00

1 line
87 B
Text

490.lean:2:0-2:19: error: invalid namespace '_root_', '_root_' is a reserved namespace