[Agda] Termination checking (perhaps could be smarter)

[Sergei Meshveliani]

On Fri, 2015-01-16 at 23:08 +0400, flicky frans wrote:
> > And what may be here a proof for that  []  is sorted?
> 
> You can write
> 
>     sort : ∀ ns -> OList (minimum ns)
> 
> and no proving is needed. 


And what is   minimum []  ?
And of course, I presume that the definition needs to be for a generic
domain A (of DecTotalOrder or such), not only for  ℕ. 


> Or you can define `OList' as
> 
>     data OList : ℕ -> List ℕ -> Set where
>       o[] : ∀ {n} -> OList n []
>       _o∷_  : ∀ {n' n ns} -> n' ≤ n -> OList n ns -> OList n' (n' ∷ ns)
> 

This does not look better than my first suggestion

 data Sorted ... : Set _  
      where
      empty  : Sorted []
      single : \forall x -> Sorted (x ∷ [])
      step   : x ≤ y -> Sorted (y ∷ ys) -> Sorted (x ∷ y ∷ ys)

(I have proved  \forall xs -> Sorted (merge-sort xs)   for such).

> I've just tried this encoding [1], but my attempt looks awkward. Maybe
> it's better to just extend `ℕ' with `ω':
> [..]

But this is not generic.

------
Sergei