Most importantly, keep track of positions when parsing and report the error, highlighting the position where it occurred. Two types of errors are reported:
unexpected input: highlight the unexpected token and suggest expected kinds of input
expected term, got formula: highlight the unexpected formula
Since applications are eagerly converted to function or predicate application depending on the expected type, "expected formula, got term" error is currently not detected. This can be improved in the future.
Most importantly, keep track of positions when parsing and report the error, highlighting the position where it occurred. Two types of errors are reported:
Since applications are eagerly converted to function or predicate application depending on the expected type, "expected formula, got term" error is currently not detected. This can be improved in the future.
Part of #86.