[Agda] Does the order of patterns matter?

[Nils Anders Danielsson]

On 2012-09-27 18:25, Altenkirch Thorsten wrote:
> However, there are many features of Agda which are not covered:
> - coinductive definitions and in particular mixed inductive-coinductive
> definitions
> - so called induction-induction which means you mutually define inductive
> types one depending on the other.
> - induction-recursion, I.e. defining an inductive type mutually with a
> recursive definition. This covers the
>    definition of universes.
>
> In these cases we don't even have an accepted set of combinators.

It's also not quite clear how to translate the use of size-change
termination into combinators (even though progress has been made
recently by Vytiniotis, Coquand and Wahlstedt: Stop when you are
Almost-Full).

-- 
/NAD