[Agda] --no-pattern-matching

[Andreas Abel]

--no-pattern-matching is an extreme form of chastity, but it should not 
hard to implement it.  If I understood correctly, you want Agda to slap 
your fingers if you wrote a constructor pattern anywhere.

The most principled way to implement this I can think of is to disallow 
any kind of splitting in the checking of function left hand sides.

Cheers,
Andreas

On 17.01.2014 15:28, Matteo Acerbi wrote:
> every now and then I would like to forbid
> myself to use pattern matching at all, at least from inside a single
> file.
>
> I would like to have the possibility to get back to that file and make
> sure that I never used pattern matching in that code just by looking
> at the OPTIONS header.
>
> I think I would find a --no-pattern-matching option, which simply
> applied this restriction, but still allowed for importing modules
> whatever their options are, very convenient.
>
> For now I am just curious as to whether others are interested: would
> anyone else like such a --no-pattern-matching option?

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/