NoTerminationCheck1.err

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