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