2 lines
91 B
Text
2 lines
91 B
Text
|
bad_id.lean:5:12: error: invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected
|