Linting proof scripts
Linting is a static analysis of finding common mistakes or improvements.
Rule 1
Successive repetition of the same goal selector or repeat
does not make sense:
foreach { foreach { ... } }
theonly { theonly { ... } }
repeat { repeat { ... } }
Rule 2
Mixture of the theonly
or foreach
is strange:
foreach { theonly { } }
theonly { foreach { } }
Rule 3
Empty blocks
Rule 4
Call to undefined function
Rule 5
Call with wrong arguments
Rule 6
Negation of match
with a using
clause.
Rule 6?
There should never be more than X branches.
Rule 7
Variable check.