[Agda] Standard WellFounded

[Sergei Meshveliani]

On Fri, 2018-08-10 at 14:06 +0100, Arseniy Alekseyev wrote:
> s/(x : X) → P a/(x : X) → P x/
> 
> On Fri, 10 Aug 2018 at 14:05, Arseniy Alekseyev
> <arseniy.alekseyev at gmail.com> wrote:
> 
>         Two things:
>         
>         
>         1.
>         In your first attempt you did not re-define GCD (or you
>         skipped that from your e-mail, but that seems to be the
>         important part). The original definition can't work because
>         [GCD x] isn't even a type so nothing can ever return a value
>         of this type.

I see now.

>         You need to define something like (I'll stubbornly keep
>         calling this P for similarity with other examples but you're
>         free to call it whatever):
>         P : Bin → Set
>         P a = (b : Bin) → GCD a b
>         
> [..]


Great! Thank you very much. It works:

-------------------------------------------------
P :  Bin → Set
P a =  (b : Bin) → GCD a b

gcd : (a : Bin) → P a
gcd =  <-rec _ P gc
  where
  gc :  (x : Bin) → (∀ x' → x' < x → P x') → P x
  gc x gcRec
       with x ≟ 0#
 
  ...  | no x≢0 =  f
                   where
                   f : P x
                   f y = liftGCD (gcRec r r<x x)
                         where
                         r   = rem y x x≢0
                         r<x = rem< y x x≢0

                         postulate  liftGCD : GCD r x → GCD x y
  ... | ...
---------------------------------------------------
     

------
Sergei