[Agda] Standard WellFounded

[Sergei Meshveliani]

On Tue, 2018-08-07 at 20:51 +0300, Sergei Meshveliani wrote:
> Dear all,
> 
> I am trying to understand how to use WellFounded of Standard library.
> 
> Can anybody demonstrate it on the following example?
> 
> --------------------------------------------------------------
> open import Function  using (_∘_)
> open import Data.List using (List; []; _∷_)
> open import Data.Bin  using (Bin; toBits; pred)
> 
> open Bin
> 
> predBin : Bin → Bin
> predBin = pred ∘ toBits
> 
> downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
> downFrom 0#      =  0# ∷ []
> downFrom (bs 1#) =  (bs 1#) ∷ (downFrom (predBin (bs 1#)))
> --------------------------------------------------------------
> 
> downFrom  is not recognized as terminating.
> How to reorganize it with using items from  
> Induction/*, WellFounded.agda ?



I presumed also that it is already given the property
  
  postulate 
    predBin-< :  (bs : List Bit) -> predBin (bs 1#) < (bs 1#) 

(I do not mean to deal here with its proof).

--
SM