[Agda] termination proof problem

[Andrea Vezzosi]

Do you also mean "y < n" ?

On Mon, Mar 28, 2016 at 5:01 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Sun, 2016-03-27 at 23:56 +0400, Sergei Meshveliani wrote:
>> Can people explain, please, the following subject concerning termination
>> proof tools?
>>
>> Having certain
>>                    P : ℕ → Set  and   P? : Decidable P,
>>
>> one needs to implement
>>
>>     search :  (n : ℕ) → ∃ \y →  m < y × P y × IsMinimalSuch y
>>
>> -- find the first  y  after  m  such that  P y.
>> [..]
>
>
> Fixing a typo:  replace  "m"  with  "n"  in these two lines.
>
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda