[Agda] Markov's principle

[Sergei Meshveliani]

People,

I have a question about Markov's principle for termination proof.

Several months ago we discussed a simple program  nextPrime  for finding
a prime natural next to the given prime  p.
It uses a bound  b  which is simple to prove, but  cnt = b - n  being
expensive to compare to 0 at run time. 

In order to have both a termination proof and fast comparison in the
loop, there were considered a counter, two bounds, and the two search
loops instead of one. 

Also Ulf Norell suggested a general approach of a large bound (say
2^1000) for the first loop. (I call this unfeasible bound). 

Now, with using the Markov's principle for termination proof, it is
possible a simpler program:

   test  n = p+1, p+2 ...  for primality, and stop when  n  is prime.

Supposing non-termination leads to contradiction to that  b > p  is
prime. Hence, the loop terminates.

So, Markov' principle is replaced in Agda with introducing an unfeasible
bound and an additional loop
--- for this particular example.

Can a replacement of this kind be made universal?
Is Markov's principle generally replaced in Agda by some approach of the
above kind?

Thanks,

------
Sergei