Menu

parsing errors

Brandon Barker

Quantification in dependent types.

Having no spaces around operators in quantification, e.g.:

{i,n:nat|i<n}

instead of:

{i,n:nat|i < n}

may result in an error along these lines:

error(parsing): the syntactic entity [s0qua] is needed.
error(parsing): the keyword '}' is needed.
error(parsing): the keyword [=] is needed.
...

Related

Wiki: Error messages