[Agda] Termination checking (perhaps could be smarter)

[Nils Anders Danielsson]

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