NoTerminationCheck2.err

NoTerminationCheck2.agda:4,1-29
The NO_TERMINATION_CHECK pragma can only preceed a mutual block or
a function definition.