[Agda] --no-pattern-matching

[Matteo Acerbi]

On Sat, Jan 18, 2014 at 12:47 AM, Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> Disallowing any kind of pattern matching is really extreme.

I agree, I only plan to use it in extreme cases. :-)

> As far as I’m concerned, I would be happy with an option limiting pattern
> matching to primitive recursion and where you can only match on one
> variable at the same time (so that any use of pattern matching would
> be equivalent to a single use of the corresponding eliminator).

I also like your proposal.

However, please consider this as an irrelevant opinion: I am not
asking Agda developers to work on this. :-)

Cheers,
Matteo