[Agda] Termination checking (perhaps could be smarter)

[flicky frans]

Sergei Meshveliani,
> 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  ℕ.

I didn't presume that.

>> 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

There are a lof of proofs, but there is no deep pattern-matching. It
looks better to me, but I'm not an expert.

>> 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.

Why not? Something like

    module DecTotalOrderω {c ℓ₁ ℓ₂} (decTotalOrder : DecTotalOrder c
ℓ₁ ℓ₂) where
      open DecTotalOrder decTotalOrder public

      open import Data.Maybe renaming (Maybe to Extended; nothing to
ω; just to liftω)
                            hiding (module Eq) public

      data _≤ω_ (i : Carrier) : Extended Carrier -> Set ℓ₂ where
        *≤ω      : i ≤ω ω
        _≤liftω_ : ∀ {j} -> i ≤ j -> i ≤ω liftω j


Nils Anders Danielsson, thanks, I'll read the paper.

2015-01-16 23:02 GMT+03:00, Nils Anders Danielsson <nad at cse.gu.se>:
> On 2015-01-15 22:22, flicky frans wrote:
>> To my small experience this is not a good way to express sortedness.
>> [...] A better definition [...] another representation [...]
>
> I've enjoyed following Conor's "pivotal" approach ("How to Keep Your
> Neighbours in Order", ICFP 2014).
>
> --
> /NAD
>