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.